Natural_deduction : FML_main.free_vars_of

let free_vars_of_fml (fml : t_fml) : t_var list =
        let rec aux (bound_vars : t_var list) (f : t_fml) : t_var list =
                match f with
                |PredApp (_, (term_list : t_term list)) ->
                        subtract (vars_of_terms term_list) bound_vars
                |UnopApp (_, fml1) ->
                        aux bound_vars fml1
                |BinopApp (_, fml1, fml2) ->
                        List.concat [aux bound_vars fml1;aux bound_vars fml2]
                |QuantApp (_, (var : t_var), fml1) ->
                        aux (var::bound_vars) fml1
        in aux [] fml