# HG changeset patch
# User wenzelm
# Date 1361795359 -3600
# Node ID cfc83ad52571ad06135bd4cf2bf3476e9854e210
# Parent  d54ee0cad2ab5a4e0b25cb6187abd852c6494d00
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;

diff -r d54ee0cad2ab -r cfc83ad52571 lib/scripts/keywords
--- a/lib/scripts/keywords	Mon Feb 25 12:52:27 2013 +0100
+++ b/lib/scripts/keywords	Mon Feb 25 13:29:19 2013 +0100
@@ -41,7 +41,6 @@
   "thy_decl" => "theory-decl",
   "thy_script" => "theory-script",
   "thy_goal" => "theory-goal",
-  "thy_schematic_goal" => "theory-goal",
   "qed_block" => "qed-block",
   "qed_global" => "qed-global",
   "prf_heading2" => "proof-heading",
diff -r d54ee0cad2ab -r cfc83ad52571 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Feb 25 12:52:27 2013 +0100
+++ b/src/Pure/Isar/keyword.ML	Mon Feb 25 13:29:19 2013 +0100
@@ -22,7 +22,6 @@
   val thy_load_files: string list -> T
   val thy_script: T
   val thy_goal: T
-  val thy_schematic_goal: T
   val qed: T
   val qed_block: T
   val qed_global: T
@@ -66,7 +65,6 @@
   val is_proof_body: string -> bool
   val is_theory_goal: string -> bool
   val is_proof_goal: string -> bool
-  val is_schematic_goal: string -> bool
   val is_qed: string -> bool
   val is_qed_global: string -> bool
 end;
@@ -104,7 +102,6 @@
 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 thy_schematic_goal = kind "thy_schematic_goal";
 val qed = kind "qed";
 val qed_block = kind "qed_block";
 val qed_global = kind "qed_global";
@@ -123,7 +120,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, thy_schematic_goal, qed, qed_block, qed_global,
+    thy_load, thy_decl, thy_script, thy_goal, qed, 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_script];
 
@@ -253,7 +250,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_schematic_goal];
+    thy_load, thy_decl, thy_script, thy_goal];
 
 val is_proof = command_category
   [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
@@ -264,9 +261,8 @@
   [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
 
-val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
+val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
-val is_schematic_goal = command_category [thy_schematic_goal];
 val is_qed = command_category [qed, qed_block];
 val is_qed_global = command_category [qed_global];
 
diff -r d54ee0cad2ab -r cfc83ad52571 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Mon Feb 25 12:52:27 2013 +0100
+++ b/src/Pure/Isar/keyword.scala	Mon Feb 25 13:29:19 2013 +0100
@@ -24,7 +24,6 @@
   val THY_LOAD = "thy_load"
   val THY_SCRIPT = "thy_script"
   val THY_GOAL = "thy_goal"
-  val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
   val QED = "qed"
   val QED_BLOCK = "qed_block"
   val QED_GLOBAL = "qed_global"
@@ -49,7 +48,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_SCHEMATIC_GOAL)
+      THY_DECL, THY_SCRIPT, THY_GOAL)
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
diff -r d54ee0cad2ab -r cfc83ad52571 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:52:27 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 13:29:19 2013 +0100
@@ -720,8 +720,7 @@
     val st' = command head_tr st;
   in
     if not future_enabled orelse is_ignored head_tr orelse
-      Keyword.is_schematic_goal (name_of head_tr) orelse null proof_trs orelse
-      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
+      null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     then
       let val (results, st'') = fold_map atom_result proof_trs st'
       in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
diff -r d54ee0cad2ab -r cfc83ad52571 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Mon Feb 25 12:52:27 2013 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Mon Feb 25 13:29:19 2013 +0100
@@ -65,7 +65,6 @@
   |> command Keyword.thy_decl         thy_decl
   |> command Keyword.thy_script       thy_decl
   |> command Keyword.thy_goal         goal
-  |> command Keyword.thy_schematic_goal goal
   |> command Keyword.qed              closegoal
   |> command Keyword.qed_block        closegoal
   |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
diff -r d54ee0cad2ab -r cfc83ad52571 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Feb 25 12:52:27 2013 +0100
+++ b/src/Pure/Pure.thy	Mon Feb 25 13:29:19 2013 +0100
@@ -50,7 +50,7 @@
   and "overloading" :: thy_decl
   and "code_datatype" :: thy_decl
   and "theorem" "lemma" "corollary" :: thy_goal
-  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
+  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
   and "notepad" :: thy_decl
   and "have" :: prf_goal % "proof"
   and "hence" :: prf_goal % "proof" == "then have"