--- a/src/HOL/Induct/Com.ML Thu May 08 10:19:52 1997 +0200
+++ b/src/HOL/Induct/Com.ML Thu May 08 10:20:37 1997 +0200
@@ -37,7 +37,7 @@
by (Blast_tac 3);
by (Blast_tac 1);
by (rewrite_goals_tac [Function_def, Unique_def]);
-(*Takes ONE MINUTE due to slow proof reconstruction*)
-by (ALLGOALS (blast_tac (!claset addEs [exec_WHILE_case])));
+by (thin_tac "(?c,s1) -[ev]-> s2" 5);
+(*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
+by (REPEAT (blast_tac (!claset addEs [exec_WHILE_case]) 1));
qed "Function_exec";
-