# HG changeset patch
# User oheimb
# Date 906650166 -7200
# Node ID dcd3e7711cac99ec7bb7df87e1cb0195cf8271f0
# Parent  ed5e19bc7e324e5ba20294172418ff489298f7a1
simplified CLASIMP_DATA
renamed mk_meta_eq to mk_eq, meta_eq to mk_meta_eq

diff -r ed5e19bc7e32 -r dcd3e7711cac src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Sep 24 17:07:24 1998 +0200
+++ b/src/HOL/simpdata.ML	Thu Sep 24 17:16:06 1998 +0200
@@ -72,16 +72,23 @@
 
 in
 
-  fun meta_eq r = r RS eq_reflection;
+(*Make meta-equalities.  The operator below is Trueprop*)
+
+  fun mk_meta_eq r = r RS eq_reflection;
 
-  fun mk_meta_eq th = case concl_of th of
+  fun mk_eq th = case concl_of th of
           Const("==",_)$_$_       => th
-      |   _$(Const("op =",_)$_$_) => meta_eq th
+      |   _$(Const("op =",_)$_$_) => mk_meta_eq th
       |   _$(Const("Not",_)$_)    => th RS not_P_imp_P_eq_False
       |   _                       => th RS P_imp_P_eq_True;
   (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
 
-  fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
+  fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
+
+  fun mk_meta_cong rl =
+    standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+    handle THM _ =>
+    error("Premises and conclusion of congruence rules must be =-equalities");
 
 
 val simp_thms = map prover
@@ -106,21 +113,17 @@
    "(? x. x=t & P(x)) = P(t)",		(*essential for termination!!*)
    "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
 
-(*Add congruence rules for = (instead of ==) *)
-infix 4 addcongs delcongs;
+(* Add congruence rules for = (instead of ==) *)
 
-fun mk_meta_cong rl =
-  standard(meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
-  handle THM _ =>
-  error("Premises and conclusion of congruence rules must be =-equalities");
-
+(* ###FIXME: Move to simplifier, 
+   taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *)
+infix 4 addcongs delcongs;
 fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
-
 fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
-
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
+
 val imp_cong = impI RSN
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
         (fn _=> [Blast_tac 1]) RS mp RS mp);
@@ -328,7 +331,7 @@
 structure SplitterData =
   struct
   structure Simplifier = Simplifier
-  val mk_meta_eq     = mk_meta_eq
+  val mk_eq          = mk_eq
   val meta_eq_to_iff = meta_eq_to_obj_eq
   val iffD           = iffD2
   val disjE          = disjE
@@ -382,10 +385,10 @@
    ("All", [spec]), ("True", []), ("False", []),
    ("If", [if_bool_eq_conj RS iffD1])];
 
-(* FIXME: move to Provers/simplifier.ML
+(* ###FIXME: move to Provers/simplifier.ML
 val mk_atomize:      (string * thm list) list -> thm -> thm list
 *)
-(* FIXME: move to Provers/simplifier.ML*)
+(* ###FIXME: move to Provers/simplifier.ML *)
 fun mk_atomize pairs =
   let fun atoms th =
         (case concl_of th of
@@ -399,7 +402,7 @@
          | _ => [th])
   in atoms end;
 
-fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
+fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
 
 fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
 				 atac, etac FalseE];
@@ -411,7 +414,7 @@
 			    setSSolver   safe_solver
 			    setSolver  unsafe_solver
 			    setmksimps (mksimps mksimps_pairs)
-			    setmkeqTrue mk_meta_eq_True;
+			    setmkeqTrue mk_eq_True;
 
 val HOL_ss = 
     HOL_basic_ss addsimps 
@@ -454,10 +457,9 @@
 (*** integration of simplifier with classical reasoner ***)
 
 structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
-  val op addcongs = op addcongs and op delcongs = op delcongs
-  and op addSaltern = op addSaltern and op addbefore = op addbefore);
-
+ (structure Simplifier = Simplifier 
+        and Classical  = Classical 
+        and Blast      = Blast);
 open Clasimp;
 
 val HOL_css = (HOL_cs, HOL_ss);