# HG changeset patch
# User paulson
# Date 863079637 -7200
# Node ID a6f73a02c619496178168c2b1e83f87fdeeecc49
# Parent  2791aa6dc1bde3c90940dcc2d8d2532490f64eb4
Made a slow proof slightly faster

diff -r 2791aa6dc1bd -r a6f73a02c619 src/HOL/Induct/Com.ML
--- 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";
-