src/HOL/Tools/res_axioms.ML
changeset 20362 bbff23c3e2ca
parent 20292 6f2b8ed987ec
child 20373 dcb321249aa9
--- a/src/HOL/Tools/res_axioms.ML	Tue Aug 08 18:40:20 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Aug 08 18:40:56 2006 +0200
@@ -347,19 +347,12 @@
 
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
 
-(*These should include any plausibly-useful theorems, especially if they need
-  Skolem functions. FIXME: this list is VERY INCOMPLETE*)
-val default_initial_thms = map pairname
-  [refl_def, antisym_def, sym_def, trans_def, single_valued_def,
-   subset_refl, Union_least, Inter_greatest];
-
 (*Setup function: takes a theory and installs ALL simprules and claset rules 
   into the clause cache*)
 fun clause_cache_setup thy =
   let val simps = simpset_rules_of_thy thy
       and clas  = claset_rules_of_thy thy
-      and thy0  = List.foldl skolem_cache thy default_initial_thms
-      val thy1  = List.foldl skolem_cache thy0 clas
+      val thy1  = List.foldl skolem_cache thy clas
   in List.foldl skolem_cache thy1 simps end;
 (*Could be duplicate theorem names, due to multiple attributes*)