diff -r 52771c21d9ca -r 14b9286ed036 simpdata.ML
--- a/simpdata.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/simpdata.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -46,8 +46,8 @@
     (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 o_apply = prove_goal HOL.thy "(f o g)(x) = f(g(x))"
- (fn _ => [ (stac o_def 1), (rtac refl 1) ]);
+val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
+ (fn _ => [rtac refl 1]);
 
 val simp_thms = map prover
  [ "(x=x) = True",
@@ -73,11 +73,11 @@
 val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
 val conj_comms = [conj_commute, conj_left_commute];
 
-val if_True = prove_goal HOL.thy "if(True,x,y) = x"
- (fn _=>[stac if_def 1,  fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
 
-val if_False = prove_goal HOL.thy "if(False,x,y) = y"
- (fn _=>[stac if_def 1,  fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
 
 val if_P = prove_goal HOL.thy "P ==> if(P,x,y) = x"
  (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
@@ -112,7 +112,7 @@
   let val lemma1 = prove_goal HOL.thy
         "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
         (fn prems => [resolve_tac prems 1, etac exI 1]);
-      val lemma2 = prove_goalw HOL.thy [Ex_def RS eq_reflection]
+      val lemma2 = prove_goalw HOL.thy [Ex_def]
         "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
         (fn prems => [REPEAT(resolve_tac prems 1)])
   in equal_intr lemma1 lemma2 end;