# HG changeset patch
# User wenzelm
# Date 1343899943 -7200
# Node ID 33f00ce23e63daf327a58ca3ca596589e9daea6c
# Parent  70a5d78e8326bbfcff0a7709aff289cffa8c77e2
more antiquotations;

diff -r 70a5d78e8326 -r 33f00ce23e63 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Aug 02 00:18:20 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 02 11:32:23 2012 +0200
@@ -256,15 +256,15 @@
 
 (* name space entry path *)
 
-fun hide_names name hide what =
-  Outer_Syntax.command (name, Keyword.thy_decl) ("hide " ^ what ^ " from name space")
+fun hide_names spec hide what =
+  Outer_Syntax.command spec ("hide " ^ what ^ " from name space")
     ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
       (Toplevel.theory o uncurry hide));
 
-val _ = hide_names "hide_class" Isar_Cmd.hide_class "classes";
-val _ = hide_names "hide_type" Isar_Cmd.hide_type "types";
-val _ = hide_names "hide_const" Isar_Cmd.hide_const "constants";
-val _ = hide_names "hide_fact" Isar_Cmd.hide_fact "facts";
+val _ = hide_names @{command_spec "hide_class"} Isar_Cmd.hide_class "classes";
+val _ = hide_names @{command_spec "hide_type"} Isar_Cmd.hide_type "types";
+val _ = hide_names @{command_spec "hide_const"} Isar_Cmd.hide_const "constants";
+val _ = hide_names @{command_spec "hide_fact"} Isar_Cmd.hide_fact "facts";
 
 
 (* use ML text *)
@@ -508,10 +508,8 @@
 
 (* statements *)
 
-fun gen_theorem schematic kind =
-  Outer_Syntax.local_theory_to_proof'
-    (if schematic then ("schematic_" ^ kind, Keyword.thy_schematic_goal)
-     else (kind, Keyword.thy_goal))
+fun gen_theorem spec schematic kind =
+  Outer_Syntax.local_theory_to_proof' spec
     ("state " ^ (if schematic then "schematic " ^ kind else kind))
     (Scan.optional (Parse_Spec.opt_thm_name ":" --|
       Scan.ahead (Parse_Spec.includes >> K "" ||
@@ -521,12 +519,12 @@
         ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
           kind NONE (K I) a includes elems concl)));
 
-val _ = gen_theorem false Thm.theoremK;
-val _ = gen_theorem false Thm.lemmaK;
-val _ = gen_theorem false Thm.corollaryK;
-val _ = gen_theorem true Thm.theoremK;
-val _ = gen_theorem true Thm.lemmaK;
-val _ = gen_theorem true Thm.corollaryK;
+val _ = gen_theorem @{command_spec "theorem"} false Thm.theoremK;
+val _ = gen_theorem @{command_spec "lemma"} false Thm.lemmaK;
+val _ = gen_theorem @{command_spec "corollary"} false Thm.corollaryK;
+val _ = gen_theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
+val _ = gen_theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
+val _ = gen_theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"