src/Provers/clasimp.ML

--- a/src/Provers/clasimp.ML	Tue Oct 24 17:34:28 2000 +0200
+++ b/src/Provers/clasimp.ML	Tue Oct 24 17:35:22 2000 +0200
@@ -31,6 +31,7 @@
   type claset
   type simpset
   type clasimpset
+  val clasimpset: unit -> clasimpset
   val addSIs2: clasimpset * thm list -> clasimpset
   val addSEs2: clasimpset * thm list -> clasimpset
   val addSDs2: clasimpset * thm list -> clasimpset
@@ -82,6 +83,8 @@
 type simpset = Simplifier.simpset;
 type clasimpset = claset * simpset;
 
+fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
+
 
 (* clasimpset operations *)
 
@@ -159,8 +162,8 @@
     ((fn (ss, _) => ss): Simplifier.simpset * thm list -> Simplifier.simpset));
 val op delIffs = foldl delIff;
 
-fun AddIffs thms = store_clasimp ((Classical.claset (), Simplifier.simpset ()) addIffs thms);
-fun DelIffs thms = store_clasimp ((Classical.claset (), Simplifier.simpset ()) delIffs thms);
+fun AddIffs thms = store_clasimp (clasimpset () addIffs thms);
+fun DelIffs thms = store_clasimp (clasimpset () delIffs thms);
 
 end;
 
@@ -176,7 +179,7 @@
 
 fun clarsimp_tac (cs, ss) = safe_asm_full_simp_tac ss THEN_ALL_NEW
                             Classical.clarify_tac (cs addSss ss);
-fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i;
+fun Clarsimp_tac i = clarsimp_tac (clasimpset ()) i;
 
 
 (* auto_tac *)
@@ -215,7 +218,7 @@
 
 fun auto_tac css = mk_auto_tac css 4 2;
 
-fun Auto_tac st = auto_tac (Classical.claset(), Simplifier.simpset()) st;
+fun Auto_tac st = auto_tac (clasimpset ()) st;
 
 fun auto () = by Auto_tac;
 
@@ -227,7 +230,7 @@
         Classical.clarify_tac cs' 1,
         IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
         ALLGOALS (Classical.first_best_tac cs')]) end;
-fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i;
+fun Force_tac i = force_tac (clasimpset ()) i;
 fun force i = by (Force_tac i);