diff -r 7949f97df77a -r 142f1eb707b4 simpdata.ML
--- a/simpdata.ML	Thu Sep 16 12:21:07 1993 +0200
+++ b/simpdata.ML	Thu Sep 16 14:29:14 1993 +0200
@@ -1,3 +1,11 @@
+(*  Title: 	HOL/simpdata.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1991  University of Cambridge
+
+Instantiation of the generic simplifier
+*)
+
 open Simplifier;
 
 local
@@ -34,10 +42,9 @@
 
 fun mk_rews thm = map mk_eq (atomize(gen_all thm));
 
-val imp_cong_lemma = impI RSN
+val imp_cong = impI RSN
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
 	(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
-val imp_meta_cong = imp_cong_lemma RS eq_reflection;
 
 val o_apply = prove_goal HOL.thy "(f o g)(x) = f(g(x))"
  (fn _ => [ (stac o_def 1), (rtac refl 1) ]);
@@ -84,15 +91,17 @@
   "[| b=c; c ==> x=u; ~c ==> y=v |] ==> if(b,x,y) = if(c,u,v)"
   (fn rew::prems =>
    [stac rew 1, stac expand_if 1, stac expand_if 1,
-    fast_tac (HOL_cs addDs prems) 1]) RS eq_reflection;
+    fast_tac (HOL_cs addDs prems) 1]);
 
+infix addcongs;
+fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
 
 val HOL_ss = empty_ss
       setmksimps mk_rews
       setsolver (fn prems => resolve_tac (TrueI::refl::prems))
       setsubgoaler asm_simp_tac
       addsimps ([if_True, if_False, o_apply] @ simp_thms)
-      addcongs [imp_meta_cong];
+      addcongs [imp_cong];
 
 fun split_tac splits =
   mk_case_split_tac (meta_obj_reflection RS iffD2) (map mk_eq splits);