1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat May 24 22:04:48 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat May 24 22:04:52 2008 +0200
     1.3 @@ -75,9 +75,8 @@
     1.4      (string * string option * mixfix) list ->
     1.5      ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     1.6      local_theory -> inductive_result * local_theory
     1.7 -  val gen_ind_decl: add_ind_def ->
     1.8 -    bool -> OuterParse.token list ->
     1.9 -    (Toplevel.transition -> Toplevel.transition) * OuterParse.token list
    1.10 +  val gen_ind_decl: add_ind_def -> bool ->
    1.11 +    OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
    1.12  end;
    1.13  
    1.14  structure InductivePackage: INDUCTIVE_PACKAGE =
    1.15 @@ -945,25 +944,21 @@
    1.16      | (a, _) => error ("Illegal local specification parameters for " ^ quote a));
    1.17  
    1.18  fun gen_ind_decl mk_def coind =
    1.19 -  P.opt_target --
    1.20    P.fixes -- P.for_fixes --
    1.21    Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
    1.22    Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
    1.23 -  >> (fn ((((loc, preds), params), specs), monos) =>
    1.24 -    Toplevel.local_theory loc
    1.25 -      (fn lthy => lthy |> gen_add_inductive mk_def true coind preds params
    1.26 -         (flatten_specification specs) monos |> snd));
    1.27 +  >> (fn (((preds, params), specs), monos) =>
    1.28 +      (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
    1.29  
    1.30  val ind_decl = gen_ind_decl add_ind_def;
    1.31  
    1.32 -val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
    1.33 -val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
    1.34 +val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
    1.35 +val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
    1.36  
    1.37  val _ =
    1.38 -  OuterSyntax.command "inductive_cases"
    1.39 +  OuterSyntax.local_theory "inductive_cases"
    1.40      "create simplified instances of elimination rules (improper)" K.thy_script
    1.41 -    (P.opt_target -- P.and_list1 SpecParse.spec
    1.42 -      >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
    1.43 +    (P.and_list1 SpecParse.spec >> (fn specs => snd o inductive_cases specs));
    1.44  
    1.45  end;
    1.46  

     2.1 --- a/src/HOL/Tools/inductive_set_package.ML	Sat May 24 22:04:48 2008 +0200
     2.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sat May 24 22:04:52 2008 +0200
     2.3 @@ -545,10 +545,10 @@
     2.4  val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
     2.5  
     2.6  val _ =
     2.7 -  OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
     2.8 +  OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
     2.9  
    2.10  val _ =
    2.11 -  OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
    2.12 +  OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
    2.13  
    2.14  end;
    2.15  

     3.1 --- a/src/HOL/Tools/recdef_package.ML	Sat May 24 22:04:48 2008 +0200
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat May 24 22:04:52 2008 +0200
     3.3 @@ -316,11 +316,10 @@
     3.4      (defer_recdef_decl >> Toplevel.theory);
     3.5  
     3.6  val _ =
     3.7 -  OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
     3.8 -    (P.opt_target --
     3.9 -      SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    3.10 -      >> (fn (((loc, thm_name), name), i) =>
    3.11 -        Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
    3.12 +  OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
    3.13 +    K.thy_goal
    3.14 +    (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    3.15 +      >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
    3.16  
    3.17  end;
    3.18  

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sat May 24 22:04:48 2008 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat May 24 22:04:52 2008 +0200
     4.3 @@ -232,55 +232,49 @@
     4.4  val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
     4.5  
     4.6  val _ =
     4.7 -  OuterSyntax.command "definition" "constant definition" K.thy_decl
     4.8 -    (P.opt_target -- constdef
     4.9 -    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition_cmd args)));
    4.10 +  OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
    4.11 +    (constdef >> (fn args => #2 o Specification.definition_cmd args));
    4.12  
    4.13  val _ =
    4.14 -  OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
    4.15 -    (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
    4.16 -    >> (fn ((loc, mode), args) =>
    4.17 -        Toplevel.local_theory loc (Specification.abbreviation_cmd mode args)));
    4.18 +  OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
    4.19 +    (opt_mode -- (Scan.option constdecl -- P.prop)
    4.20 +    >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
    4.21  
    4.22  val _ =
    4.23 -  OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl
    4.24 -    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    4.25 -    >> (fn ((loc, mode), args) =>
    4.26 -        Toplevel.local_theory loc (Specification.notation_cmd true mode args)));
    4.27 +  OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
    4.28 +    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    4.29 +    >> (fn (mode, args) => Specification.notation_cmd true mode args));
    4.30  
    4.31  val _ =
    4.32 -  OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl
    4.33 -    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    4.34 -    >> (fn ((loc, mode), args) =>
    4.35 -        Toplevel.local_theory loc (Specification.notation_cmd false mode args)));
    4.36 +  OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl
    4.37 +    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    4.38 +    >> (fn (mode, args) => Specification.notation_cmd false mode args));
    4.39  
    4.40  
    4.41  (* constant specifications *)
    4.42  
    4.43  val _ =
    4.44 -  OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
    4.45 -    (P.opt_target --
    4.46 -     (Scan.optional P.fixes [] --
    4.47 -      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
    4.48 -    >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization_cmd x y)));
    4.49 +  OuterSyntax.local_theory "axiomatization" "axiomatic constant specification" K.thy_decl
    4.50 +    (Scan.optional P.fixes [] --
    4.51 +      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) []
    4.52 +    >> (fn (x, y) => #2 o Specification.axiomatization_cmd x y));
    4.53  
    4.54  
    4.55  (* theorems *)
    4.56  
    4.57 -fun theorems kind = P.opt_target -- SpecParse.name_facts
    4.58 -  >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems_cmd kind args));
    4.59 +fun theorems kind =
    4.60 +  SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
    4.61  
    4.62  val _ =
    4.63 -  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
    4.64 +  OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
    4.65  
    4.66  val _ =
    4.67 -  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
    4.68 +  OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
    4.69  
    4.70  val _ =
    4.71 -  OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl
    4.72 -    (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
    4.73 -      >> (fn (loc, args) => Toplevel.local_theory loc
    4.74 -          (#2 o Specification.theorems_cmd "" [(("", []), args)])));
    4.75 +  OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
    4.76 +    (P.and_list1 SpecParse.xthms1
    4.77 +      >> (fn args => #2 o Specification.theorems_cmd "" [(("", []), flat args)]));
    4.78  
    4.79  
    4.80  (* name space entry path *)
    4.81 @@ -328,16 +322,14 @@
    4.82      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
    4.83  
    4.84  val _ =
    4.85 -  OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
    4.86 -    (P.opt_target -- P.position P.text
    4.87 -    >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
    4.88 +  OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
    4.89 +    (P.position P.text >> IsarCmd.declaration);
    4.90  
    4.91  val _ =
    4.92 -  OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
    4.93 -    (P.opt_target --
    4.94 -      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
    4.95 +  OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
    4.96 +    (P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
    4.97        P.position P.text -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
    4.98 -    >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
    4.99 +    >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
   4.100  
   4.101  
   4.102  (* translation functions *)
   4.103 @@ -439,9 +431,8 @@
   4.104            (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
   4.105  
   4.106  val _ =
   4.107 -  OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal
   4.108 -    (P.opt_target -- P.xname >> (fn (loc, class) =>
   4.109 -      Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
   4.110 +  OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
   4.111 +    (P.xname >> Subclass.subclass_cmd);
   4.112  
   4.113  val _ =
   4.114    OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
   4.115 @@ -482,13 +473,11 @@
   4.116  (* statements *)
   4.117  
   4.118  fun gen_theorem kind =
   4.119 -  OuterSyntax.command kind ("state " ^ kind) K.thy_goal
   4.120 -    (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
   4.121 +  OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
   4.122 +    (Scan.optional (SpecParse.opt_thm_name ":" --|
   4.123        Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
   4.124 -      SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
   4.125 -      (Toplevel.print o
   4.126 -       Toplevel.local_theory_to_proof' loc
   4.127 -         (Specification.theorem_cmd kind NONE (K I) a elems concl))));
   4.128 +      SpecParse.general_statement >> (fn (a, (elems, concl)) =>
   4.129 +        (Specification.theorem_cmd kind NONE (K I) a elems concl)));
   4.130  
   4.131  val _ = gen_theorem Thm.theoremK;
   4.132  val _ = gen_theorem Thm.lemmaK;