# HG changeset patch
# User paulson
# Date 841912160 -7200
# Node ID 97f1c6bf3acece774a8418b7842401d73400b560
# Parent  1badf0b0804084827fdbc9be2e8f3a8c597c385d
Miniscoping rules are deleted, as these brittle proofs
would otherwise have to be entirely redone

diff -r 1badf0b08040 -r 97f1c6bf3ace src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Thu Sep 05 10:27:36 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Thu Sep 05 10:29:20 1996 +0200
@@ -6,6 +6,8 @@
 Main result: auto_chopper satisfies the is_auto_chopper specification.
 *)
 
+Delsimps (ex_simps @ all_simps);
+
 open AutoChopper;
 
 infix repeat_RS;
diff -r 1badf0b08040 -r 97f1c6bf3ace src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Thu Sep 05 10:27:36 1996 +0200
+++ b/src/HOL/MiniML/W.ML	Thu Sep 05 10:29:20 1996 +0200
@@ -9,6 +9,7 @@
 open W;
 
 Addsimps [Suc_le_lessD];
+Delsimps (ex_simps @ all_simps);
 
 (* correctness of W with respect to has_type *)
 goal W.thy