src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 38285 e2d546a07fa2
parent 38280 ecae87b9b9c4
child 38286 174568533593
     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, [])