# HG changeset patch
# User paulson
# Date 831635100 -7200
# Node ID b50755328aadc70d281db3effc85fc54adec0edd
# Parent  35961ebbbfad5558db3b8cea6220969b2afcfc2c
Updated for new form of induction rules

diff -r 35961ebbbfad -r b50755328aad src/ZF/Coind/MT.ML
--- a/src/ZF/Coind/MT.ML	Thu May 09 11:43:44 1996 +0200
+++ b/src/ZF/Coind/MT.ML	Thu May 09 11:45:00 1996 +0200
@@ -156,11 +156,10 @@
 
 fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac)); 
 
-val prems = goal MT.thy 
-  "<ve,e,v>:EvalRel ==>         \
-\  (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
-by (rtac (EvalRel.mutual_induct RS spec RS spec RS spec RS impE) 1);
-by (resolve_tac prems 7 THEN assume_tac 7);
+goal MT.thy 
+  "!!e. <ve,e,v>:EvalRel ==>         \
+\       (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
+by (etac EvalRel.induct 1);
 by (safe_tac ZF_cs);
 by (mt_cases_tac consistency_const);
 by (mt_cases_tac consistency_var);