src/Pure/Isar/keyword.ML

   val thy_heading3: T
   val thy_heading4: T
   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
   val qed_block: T
   val qed_global: T

 val thy_heading3 = kind "thy_heading3";
 val thy_heading4 = kind "thy_heading4";
 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";
 val qed_block = kind "qed_block";
 val qed_global = kind "qed_global";

 val prf_asm_goal_script = kind "prf_asm_goal_script";
 val prf_script = kind "prf_script";
 
 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];
 
 
 (* tags *)

 
 val is_theory_load = command_category [thy_load];
 
 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,
     prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
     prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];