1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 16:54:12 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 17:38:40 2010 +0200
1.3 @@ -401,11 +401,6 @@
1.4 class_rel_clauses, arity_clauses))
1.5 end
1.6
1.7 -val axiom_prefix = "ax_"
1.8 -val conjecture_prefix = "conj_"
1.9 -val arity_clause_prefix = "clsarity_"
1.10 -val tfrees_name = "tfrees"
1.11 -
1.12 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
1.13
1.14 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])