# HG changeset patch
# User paulson
# Date 881919165 -3600
# Node ID 57e16404c2a92b7e1a146af3633b862ba6d05826
# Parent  1865cb8df1165e4d6af5a32485f57aaa796921d8
ugly patch for new Blast_tac

diff -r 1865cb8df116 -r 57e16404c2a9 src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Fri Dec 12 10:31:25 1997 +0100
+++ b/src/HOL/Induct/Com.ML	Fri Dec 12 10:32:45 1997 +0100
@@ -38,6 +38,7 @@
 by (Blast_tac 1);
 by (rewrite_goals_tac [Function_def, Unique_def]);
 by (thin_tac "(?c,s1) -[ev]-> s2" 5);
+by (rotate_tac 1 5);   (*PATCH to avoid very slow proof*)
 (*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";