src/Provers/classical.ML

--- a/src/Provers/classical.ML	Mon Aug 20 20:38:32 2007 +0200
+++ b/src/Provers/classical.ML	Mon Aug 20 20:43:58 2007 +0200
@@ -655,22 +655,24 @@
   Merging the term nets may look more efficient, but the rather delicate
   treatment of priority might get muddled up.*)
 fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
-    CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
+    cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
       swrappers, uwrappers, ...}) =
-  let
-    val safeIs' = fold rem_thm safeIs safeIs2;
-    val safeEs' = fold rem_thm safeEs safeEs2;
-    val hazIs' = fold rem_thm hazIs hazIs2;
-    val hazEs' = fold rem_thm hazEs hazEs2;
-    val cs1   = cs addSIs safeIs'
-                   addSEs safeEs'
-                   addIs  hazIs'
-                   addEs  hazEs';
-    val cs2 = map_swrappers
-      (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
-    val cs3 = map_uwrappers
-      (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
-  in cs3 end;
+  if pointer_eq (cs, cs') then cs
+  else
+    let
+      val safeIs' = fold rem_thm safeIs safeIs2;
+      val safeEs' = fold rem_thm safeEs safeEs2;
+      val hazIs' = fold rem_thm hazIs hazIs2;
+      val hazEs' = fold rem_thm hazEs hazEs2;
+      val cs1   = cs addSIs safeIs'
+                     addSEs safeEs'
+                     addIs  hazIs'
+                     addEs  hazEs';
+      val cs2 = map_swrappers
+        (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
+      val cs3 = map_uwrappers
+        (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
+    in cs3 end;
 
 
 (**** Simple tactics for theorem proving ****)
@@ -851,12 +853,14 @@
 val empty_context_cs = make_context_cs ([], []);
 
 fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
-  let
-    val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
-    val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
-    val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
-    val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
-  in make_context_cs (swrappers', uwrappers') end;
+  if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
+  else
+    let
+      val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
+      val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
+      val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
+      val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
+    in make_context_cs (swrappers', uwrappers') end;