tuned merge operations via pointer_eq;

--- 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;
 
 
 

--- a/src/Pure/meta_simplifier.ML	Mon Aug 20 20:38:32 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Aug 20 20:43:58 2007 +0200
@@ -791,28 +791,30 @@
 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
 
 fun merge_ss (ss1, ss2) =
-  let
-    val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
-     {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
-      loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
-    val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
-     {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
-      loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
-
-    val rules' = Net.merge eq_rrule (rules1, rules2);
-    val prems' = merge Thm.eq_thm_prop (prems1, prems2);
-    val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
-    val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
-    val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
-    val weak' = merge (op =) (weak1, weak2);
-    val procs' = Net.merge eq_proc (procs1, procs2);
-    val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
-    val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
-    val solvers' = merge eq_solver (solvers1, solvers2);
-  in
-    make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
-      mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
-  end;
+  if pointer_eq (ss1, ss2) then ss1
+  else
+    let
+      val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
+       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
+        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
+      val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
+       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
+        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
+  
+      val rules' = Net.merge eq_rrule (rules1, rules2);
+      val prems' = merge Thm.eq_thm_prop (prems1, prems2);
+      val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
+      val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
+      val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
+      val weak' = merge (op =) (weak1, weak2);
+      val procs' = Net.merge eq_proc (procs1, procs2);
+      val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
+      val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
+      val solvers' = merge eq_solver (solvers1, solvers2);
+    in
+      make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
+        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
+    end;