# HG changeset patch
# User wenzelm
# Date 968352782 -7200
# Node ID 1319676eb2db66bfc46bc010b387f69f6c4d7ab5
# Parent  75e55370b1aef5ffa6b82c234609520cd7f598d9
chop_nonempty: accomodate new qed_spec_mp;

diff -r 75e55370b1ae -r 1319676eb2db src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Thu Sep 07 20:52:02 2000 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Thu Sep 07 20:53:02 2000 +0200
@@ -54,7 +54,7 @@
 by (etac exE 1);
 by (etac allE 1);
 by Auto_tac;
-qed_spec_mp "chop_nonempty";
+qed "chop_nonempty";
 
 val [prem] = goalw thy [is_maxchopper_def]
  "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
@@ -63,7 +63,7 @@
  by (rtac conjI 1);
   by (etac (prem RS chop_concat) 1);
  by (rtac conjI 1);
-  by (etac (prem RS chop_nonempty) 1);
+  by (etac (prem RS (chop_nonempty RS spec RS spec RS mp)) 1);
  by (etac rev_mp 1);
  by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
  by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]