# HG changeset patch
# User paulson
# Date 916225731 -3600
# Node ID 45958e54d72e8dc8f74f3a6da2090f74d09af699
# Parent  b321f5aaa5f42888e405022e41082447fb57e33e
congruence rules finally use == instead of = and <->

diff -r b321f5aaa5f4 -r 45958e54d72e src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Jan 13 12:08:18 1999 +0100
+++ b/src/FOL/simpdata.ML	Wed Jan 13 12:08:51 1999 +0100
@@ -90,8 +90,15 @@
   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
   | _                           => th RS iff_reflection_T;
 
-fun mk_meta_cong rl = standard (mk_meta_eq rl); 
-(*FIXME: how about the premises?*)
+(*Replace premises x=y, X<->Y by X==Y*)
+val mk_meta_prems = 
+    rule_by_tactic 
+      (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
+
+fun mk_meta_cong rl =
+  standard(mk_meta_eq (mk_meta_prems rl))
+  handle THM _ =>
+  error("Premises and conclusion of congruence rules must use =-equality or <->");
 
 val mksimps_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
@@ -209,11 +216,6 @@
     "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
 
 
-(*Used in ZF, perhaps elsewhere?*)
-val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
-  (fn [prem] => [rewtac prem, rtac refl 1]);
-
-
 (** make simplification procedures for quantifier elimination **)
 structure Quantifier1 = Quantifier1Fun(
 struct
@@ -307,11 +309,11 @@
     True_implies_equals];  (* prune asms `True' *)
 
 val IFOL_simps =
-   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
+    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     imp_simps @ iff_simps @ quant_simps;
 
 val notFalseI = int_prove_fun "~False";
-val triv_rls = [TrueI,refl,iff_refl,notFalseI];
+val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI];
 
 fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
 				 atac, etac FalseE];