# HG changeset patch
# User lcp
# Date 768067214 -7200
# Node ID 0aeff597d4b12c8fc0ed90ea2763a05fff66ab9d
# Parent  2b74eebdbdb81da660139084f0916e9e9674b6e1
CTT.ML/SumE_fst,SumE_snd: tidied

diff -r 2b74eebdbdb8 -r 0aeff597d4b1 src/CTT/CTT.ML
--- a/src/CTT/CTT.ML	Wed May 04 17:47:30 1994 +0200
+++ b/src/CTT/CTT.ML	Wed May 04 18:00:14 1994 +0200
@@ -222,27 +222,20 @@
 
 (** The elimination rules for fst/snd **)
 
-val SumE_fst = prove_goal CTT.thy 
+val SumE_fst = prove_goalw CTT.thy basic_defs
     "p : Sum(A,B) ==> fst(p) : A"
- (fn prems=>
-  [ (rewrite_goals_tac basic_defs),
-    (resolve_tac elim_rls 1),
-    (REPEAT (pc_tac prems 1)),
-    (fold_tac basic_defs) ]);
+ (fn [major] =>
+  [ (rtac (major RS SumE) 1),
+    (assume_tac 1) ]);
 
 (*The first premise must be p:Sum(A,B) !!*)
-val SumE_snd = prove_goal CTT.thy 
+val SumE_snd = prove_goalw CTT.thy basic_defs
     "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
 \    |] ==> snd(p) : B(fst(p))"
- (fn prems=>
-  [ (rewrite_goals_tac basic_defs),
-    (resolve_tac elim_rls 1),
-    (resolve_tac prems 1),
-    (resolve_tac [replace_type] 1),
-    (resolve_tac [subst_eqtyparg] 1),   (*like B(x) equality formation?*)
-    (resolve_tac comp_rls 1),
-    (typechk_tac prems),
-    (fold_tac basic_defs) ]);
+ (fn major::prems=>
+  [ (rtac (major RS SumE) 1),
+    (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1),
+    (typechk_tac prems) ]);
 
 end;