src/HOL/Tools/Sledgehammer/sledgehammer.ML

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