# HG changeset patch
# User wenzelm
# Date 1394808089 -3600
# Node ID 8453d35e4684650e1347c27821f0c6f146455f01
# Parent  a200bffe402793f618753a5a03b6ce5fd6690d78
discontinued somewhat pointless "thy_script" keyword kind;

diff -r a200bffe4027 -r 8453d35e4684 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Fri Mar 14 15:26:52 2014 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Mar 14 15:41:29 2014 +0100
@@ -367,6 +367,7 @@
     "hide_fact"
     "hide_type"
     "inductive"
+    "inductive_cases"
     "instantiation"
     "judgment"
     "lemmas"
@@ -404,7 +405,7 @@
     "typedecl"))
 
 (defconst isar-keywords-theory-script
-  '("inductive_cases"))
+  '())
 
 (defconst isar-keywords-theory-goal
   '("corollary"
diff -r a200bffe4027 -r 8453d35e4684 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Mar 14 15:26:52 2014 +0100
+++ b/etc/isar-keywords.el	Fri Mar 14 15:41:29 2014 +0100
@@ -530,7 +530,9 @@
     "import_tptp"
     "import_type_map"
     "inductive"
+    "inductive_cases"
     "inductive_set"
+    "inductive_simps"
     "instantiation"
     "judgment"
     "lemmas"
@@ -590,8 +592,7 @@
     "typedecl"))
 
 (defconst isar-keywords-theory-script
-  '("inductive_cases"
-    "inductive_simps"))
+  '())
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
diff -r a200bffe4027 -r 8453d35e4684 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Mar 14 15:26:52 2014 +0100
+++ b/src/HOL/Inductive.thy	Fri Mar 14 15:41:29 2014 +0100
@@ -7,8 +7,8 @@
 theory Inductive
 imports Complete_Lattices Ctr_Sugar
 keywords
-  "inductive" "coinductive" :: thy_decl and
-  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+  "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
+  "monos" and
   "print_inductives" :: diag and
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
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,
diff -r a200bffe4027 -r 8453d35e4684 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Mar 14 15:41:29 2014 +0100
@@ -22,7 +22,6 @@
   val THY_HEADING4 = "thy_heading4"
   val THY_DECL = "thy_decl"
   val THY_LOAD = "thy_load"
-  val THY_SCRIPT = "thy_script"
   val THY_GOAL = "thy_goal"
   val QED = "qed"
   val QED_SCRIPT = "qed_script"
@@ -50,7 +49,7 @@
   val diag = Set(DIAG)
   val theory =
     Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
-      THY_DECL, THY_SCRIPT, THY_GOAL)
+      THY_DECL, THY_GOAL)
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
@@ -61,6 +60,5 @@
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
       PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
-  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }
 
diff -r a200bffe4027 -r 8453d35e4684 src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Pure/Tools/keywords.scala	Fri Mar 14 15:41:29 2014 +0100
@@ -25,7 +25,6 @@
     "thy_heading4" -> "theory-heading",
     "thy_load" -> "theory-decl",
     "thy_decl" -> "theory-decl",
-    "thy_script" -> "theory-script",
     "thy_goal" -> "theory-goal",
     "qed_script" -> "qed",
     "qed_block" -> "qed-block",
diff -r a200bffe4027 -r 8453d35e4684 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 14 15:26:52 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 14 15:41:29 2014 +0100
@@ -53,7 +53,6 @@
     import JEditToken._
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
-      Keyword.THY_SCRIPT -> LABEL,
       Keyword.QED_SCRIPT -> DIGIT,
       Keyword.PRF_SCRIPT -> DIGIT,
       Keyword.PRF_ASM -> KEYWORD3,
diff -r a200bffe4027 -r 8453d35e4684 src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Fri Mar 14 15:26:52 2014 +0100
+++ b/src/ZF/Inductive_ZF.thy	Fri Mar 14 15:41:29 2014 +0100
@@ -14,8 +14,7 @@
 theory Inductive_ZF
 imports Fixedpt QPair Nat_ZF
 keywords
-  "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
-  "inductive_cases" :: thy_script and
+  "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
   "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   "elimination" "induction" "case_eqns" "recursor_eqns"
 begin