src/HOL/Lex/AutoMaxChop.ML

--- a/src/HOL/Lex/AutoMaxChop.ML	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoMaxChop.ML	Thu Mar 04 10:04:42 2004 +0100
@@ -14,12 +14,12 @@
 by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
-                           delsimps [delta_append]) 1);
+                           delsimps [thm"delta_append"]) 1);
 qed_spec_mp "auto_split_lemma";
 
-Goalw [accepts_def]
+Goalw [thm"accepts_def"]
  "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
-by (stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
+by (stac ((read_instantiate [("s","start A")] (thm"delta_Nil")) RS sym) 1);
 by (stac auto_split_lemma 1);
 by (Simp_tac 1);
 qed_spec_mp "auto_split_is_maxsplit";
@@ -27,11 +27,11 @@
 Goal
  "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
 by (simp_tac (simpset() addsimps
-        [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
+        [auto_split_is_maxsplit,thm"is_maxsplitter_maxsplit"]) 1);
 qed "is_maxsplitter_auto_split";
 
-Goalw [auto_chop_def]
+Goalw [thm"auto_chop_def"]
  "is_maxchopper (accepts A) (auto_chop A)";
-by (rtac is_maxchopper_chop 1);
+by (rtac (thm"is_maxchopper_chop") 1);
 by (rtac is_maxsplitter_auto_split 1);
 qed "is_maxchopper_auto_chop";