# HG changeset patch
# User wenzelm
# Date 1136567892 -3600
# Node ID e0d509b1df1dd6576c2277f301870f11a8506d19
# Parent  4ce4dba4af0786dfe3f08807d228511dde0eb827
obsolete, reuse mk_rews of local simpset;

diff -r 4ce4dba4af07 -r e0d509b1df1d src/FOL/eqrule_FOL_data.ML
--- a/src/FOL/eqrule_FOL_data.ML	Fri Jan 06 15:18:22 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  ID:         $Id$
-    Author:     Lucas Dixon, University of Edinburgh
-                lucas.dixon@ed.ac.uk
-    Created:    18 Feb 2004
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  DESCRIPTION:
-
-    Data for equality rules in the logic
-
-*)   
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-structure ZF_EqRuleData : EQRULE_DATA =
-struct
-
-fun mk_eq th = case concl_of th of
-        Const("==",_)$_$_       => SOME (th)
-    |   _$(Const("op <->",_)$_$_) => SOME (th RS iff_reflection)
-    |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
-    |   _ => NONE;
-
-val tranformation_pairs =
-  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
-   ("All", [spec]), ("True", []), ("False", [])];
-
-(*
-val mk_atomize:      (string * thm list) list -> thm -> thm list
-looks too specific to move it somewhere else
-*)
-fun mk_atomize pairs =
-  let fun atoms th =
-        (case Thm.concl_of th of
-           Const("Trueprop",_) $ p =>
-             (case Term.head_of p of
-                Const(a,_) =>
-                  (case AList.lookup (op =) pairs a of
-                     SOME rls => List.concat (map atoms ([th] RL rls))
-                   | NONE => [th])
-              | _ => [th])
-         | _ => [th])
-  in atoms end;
-
-val prep_meta_eq = 
-    (List.mapPartial  
-       mk_eq
-       o (mk_atomize tranformation_pairs)
-       o Drule.gen_all 
-       o zero_var_indexes)
-
-end;
-
-structure EqSubst = EqSubstFun(ZF_EqRuleData);
diff -r 4ce4dba4af07 -r e0d509b1df1d src/HOL/eqrule_HOL_data.ML
--- a/src/HOL/eqrule_HOL_data.ML	Fri Jan 06 15:18:22 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  ID:		$Id$
-    Author:     Lucas Dixon, University of Edinburgh
-                lucas.dixon@ed.ac.uk
-    Modified:   22 July 2004
-    Created:    18 Feb 2004
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  DESCRIPTION:
-
-    Data for equality rules in the logic
-
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-structure HOL_EqRuleData : EQRULE_DATA =
-struct
-
-val eq_reflection = thm "eq_reflection";
-val mp = thm "mp";
-val spec = thm "spec";
-val if_bool_eq_conj = thm "if_bool_eq_conj";
-val iffD1 = thm "iffD1";
-val conjunct2 = thm "conjunct2";
-val conjunct1 = thm "conjunct1";
-
-fun mk_eq th = case concl_of th of
-        Const("==",_)$_$_       => SOME (th)
-    |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
-    |   _ => NONE;
-
-val tranformation_pairs =
-  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
-   ("All", [spec]), ("True", []), ("False", []),
-   ("HOL.If", [if_bool_eq_conj RS iffD1])];
-
-(*
-val mk_atomize:      (string * thm list) list -> thm -> thm list
-looks too specific to move it somewhere else
-*)
-fun mk_atomize pairs =
-  let fun atoms th =
-        (case Thm.concl_of th of
-           Const("Trueprop",_) $ p =>
-             (case Term.head_of p of
-                Const(a,_) =>
-                  (case AList.lookup (op =) pairs a of
-                     SOME rls => List.concat (map atoms ([th] RL rls))
-                   | NONE => [th])
-              | _ => [th])
-         | _ => [th])
-  in atoms end;
-
-val prep_meta_eq = 
-    (List.mapPartial  
-       mk_eq
-       o (mk_atomize tranformation_pairs)
-       o Drule.gen_all 
-       o zero_var_indexes)
-
-end;
-
-structure EqSubst = EqSubstFun(HOL_EqRuleData);