diff -r a200bffe4027 -r 8453d35e4684 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Mar 14 15:41:29 2014 +0100
@@ -20,7 +20,6 @@
   val thy_decl: T
   val thy_load: T
   val thy_load_files: string list -> T
-  val thy_script: T
   val thy_goal: T
   val qed: T
   val qed_script: T
@@ -101,7 +100,6 @@
 val thy_decl = kind "thy_decl";
 val thy_load = kind "thy_load";
 fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
-val thy_script = kind "thy_script";
 val thy_goal = kind "thy_goal";
 val qed = kind "qed";
 val qed_script = kind "qed_script";
@@ -123,7 +121,7 @@
 
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
+    thy_load, thy_decl, thy_goal, qed, qed_script, qed_block, qed_global,
     prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
@@ -249,7 +247,7 @@
 
 val is_theory = command_category
   [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal];
+    thy_load, thy_decl, thy_goal];
 
 val is_proof = command_category
   [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,