modernized structure Reorient_Proc;
explicit merge of constituent functions, avoids exponential blowup when traversing the import graph;
adapted Theory_Data;
tuned;

--- a/src/HOL/HOL.thy	Sun Nov 08 18:43:42 2009 +0100
+++ b/src/HOL/HOL.thy	Sun Nov 08 19:15:37 2009 +0100
@@ -1480,40 +1480,35 @@
 ML {*
 signature REORIENT_PROC =
 sig
-  val init : theory -> theory
   val add : (term -> bool) -> theory -> theory
   val proc : morphism -> simpset -> cterm -> thm option
 end;
 
-structure ReorientProc : REORIENT_PROC =
+structure Reorient_Proc : REORIENT_PROC =
 struct
-  structure Data = TheoryDataFun
+  structure Data = Theory_Data
   (
-    type T = term -> bool;
-    val empty = (fn _ => false);
-    val copy = I;
+    type T = ((term -> bool) * stamp) list;
+    val empty = [];
     val extend = I;
-    fun merge _ (m1, m2) = (fn t => m1 t orelse m2 t);
-  )
+    fun merge data : T = Library.merge (eq_snd op =) data;
+  );
+  fun add m = Data.map (cons (m, stamp ()));
+  fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
 
-  val init = Data.init;
-  fun add m = Data.map (fn matches => fn t => matches t orelse m t);
   val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
   fun proc phi ss ct =
     let
       val ctxt = Simplifier.the_context ss;
       val thy = ProofContext.theory_of ctxt;
-      val matches = Data.get thy;
     in
       case Thm.term_of ct of
-        (_ $ t $ u) => if matches u then NONE else SOME meta_reorient
+        (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient
       | _ => NONE
     end;
 end;
 *}
 
-setup ReorientProc.init
-
 
 subsection {* Other simple lemmas and lemma duplicates *}
 
@@ -1560,14 +1555,14 @@
   unfolding Let_def ..
 
 setup {*
-  ReorientProc.add
+  Reorient_Proc.add
     (fn Const(@{const_name HOL.zero}, _) => true
       | Const(@{const_name HOL.one}, _) => true
       | _ => false)
 *}
 
-simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
-simproc_setup reorient_one ("1 = x") = ReorientProc.proc
+simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
+simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
 
 typed_print_translation {*
 let

--- a/src/HOL/Int.thy	Sun Nov 08 18:43:42 2009 +0100
+++ b/src/HOL/Int.thy	Sun Nov 08 19:15:37 2009 +0100
@@ -1502,11 +1502,11 @@
 declaration {* K Int_Arith.setup *}
 
 setup {*
-  ReorientProc.add
+  Reorient_Proc.add
     (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
 *}
 
-simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
+simproc_setup reorient_numeral ("number_of w = x") = Reorient_Proc.proc
 
 
 subsection{*Lemmas About Small Numerals*}

--- a/src/HOL/ex/Numeral.thy	Sun Nov 08 18:43:42 2009 +0100
+++ b/src/HOL/ex/Numeral.thy	Sun Nov 08 19:15:37 2009 +0100
@@ -923,22 +923,21 @@
 
 declare Suc_of_num [simp]
 
-thm numeral
-
 
 subsection {* Simplification Procedures *}
 
 subsubsection {* Reorientation of equalities *}
 
 setup {*
-  ReorientProc.add
+  Reorient_Proc.add
     (fn Const(@{const_name of_num}, _) $ _ => true
       | Const(@{const_name uminus}, _) $
           (Const(@{const_name of_num}, _) $ _) => true
       | _ => false)
 *}
 
-simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc
+simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = Reorient_Proc.proc
+
 
 subsubsection {* Constant folding for multiplication in semirings *}
 

--- a/src/HOLCF/Pcpo.thy	Sun Nov 08 18:43:42 2009 +0100
+++ b/src/HOLCF/Pcpo.thy	Sun Nov 08 19:15:37 2009 +0100
@@ -196,11 +196,11 @@
 text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
 
 setup {*
-  ReorientProc.add
+  Reorient_Proc.add
     (fn Const(@{const_name UU}, _) => true | _ => false)
 *}
 
-simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
+simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
 
 context pcpo
 begin