diff --git a/src/core/decl.ml b/src/core/decl.ml index bd3627cbe0d5c22cea6759e7fe59a615f82d436e..39e3ef737bba938ad4d04ea42b892955e724ae4e 100644 --- a/src/core/decl.ml +++ b/src/core/decl.ml @@ -47,6 +47,9 @@ let check_vl ty v = ty_equal_check ty v.vs_ty let check_tl ty t = ty_equal_check ty (t_type t) let make_ls_defn ls vl t = + (* check for duplicate arguments *) + let add_v s v = Svs.add_new v (DuplicateVar v) s in + ignore (List.fold_left add_v Svs.empty vl); (* build the definition axiom *) let hd = t_app ls (List.map t_var vl) t.t_ty in let bd = TermTF.t_selecti t_equ t_iff hd t in