# HG changeset patch
# User paulson
# Date 920455949 -3600
# Node ID 3815b5b095cb2d757a7597368a754da0dc9a3372
# Parent  1a88db6e7c7ecd73fbf65b9b78253601b3f02b7d
tidied

diff -r 1a88db6e7c7e -r 3815b5b095cb src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Wed Mar 03 10:50:42 1999 +0100
+++ b/src/HOL/Induct/Com.ML	Wed Mar 03 11:12:29 1999 +0100
@@ -38,9 +38,6 @@
 by (Blast_tac 3);
 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";