# HG changeset patch
# User nipkow
# Date 889557844 -3600
# Node ID 6b7027b9e3f405c86c44ed49dc0a2c0a138e8756
# Parent  7edba45a699836b15a1355237e098ba3c523651b
Mod because of not1_or.

diff -r 7edba45a6998 -r 6b7027b9e3f4 src/HOL/Lex/MaxPrefix.ML
--- a/src/HOL/Lex/MaxPrefix.ML	Tue Mar 10 19:15:00 1998 +0100
+++ b/src/HOL/Lex/MaxPrefix.ML	Tue Mar 10 20:24:04 1998 +0100
@@ -41,9 +41,8 @@
   be disjE 1;
    by(Clarify_tac 1);
    by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
+  by(Blast_tac 1);
  by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
 by(subgoal_tac "~P(ps)" 1);
 by(Asm_simp_tac 1);
 by(fast_tac (claset() addss simpset()) 1);