more uniform treatment of OuterSyntax.local_theory commands;

--- a/src/HOL/Tools/inductive_package.ML	Sat May 24 22:04:48 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat May 24 22:04:52 2008 +0200
@@ -75,9 +75,8 @@
     (string * string option * mixfix) list ->
     ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> inductive_result * local_theory
-  val gen_ind_decl: add_ind_def ->
-    bool -> OuterParse.token list ->
-    (Toplevel.transition -> Toplevel.transition) * OuterParse.token list
+  val gen_ind_decl: add_ind_def -> bool ->
+    OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
 end;
 
 structure InductivePackage: INDUCTIVE_PACKAGE =
@@ -945,25 +944,21 @@
     | (a, _) => error ("Illegal local specification parameters for " ^ quote a));
 
 fun gen_ind_decl mk_def coind =
-  P.opt_target --
   P.fixes -- P.for_fixes --
   Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
   Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
-  >> (fn ((((loc, preds), params), specs), monos) =>
-    Toplevel.local_theory loc
-      (fn lthy => lthy |> gen_add_inductive mk_def true coind preds params
-         (flatten_specification specs) monos |> snd));
+  >> (fn (((preds, params), specs), monos) =>
+      (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
 
 val ind_decl = gen_ind_decl add_ind_def;
 
-val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
-val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
+val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
 
 val _ =
-  OuterSyntax.command "inductive_cases"
+  OuterSyntax.local_theory "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.opt_target -- P.and_list1 SpecParse.spec
-      >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
+    (P.and_list1 SpecParse.spec >> (fn specs => snd o inductive_cases specs));
 
 end;
 

--- a/src/HOL/Tools/inductive_set_package.ML	Sat May 24 22:04:48 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Sat May 24 22:04:52 2008 +0200
@@ -545,10 +545,10 @@
 val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
 
 val _ =
-  OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
+  OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
 
 val _ =
-  OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
+  OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
 
 end;
 

--- a/src/HOL/Tools/recdef_package.ML	Sat May 24 22:04:48 2008 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat May 24 22:04:52 2008 +0200
@@ -316,11 +316,10 @@
     (defer_recdef_decl >> Toplevel.theory);
 
 val _ =
-  OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
-    (P.opt_target --
-      SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
-      >> (fn (((loc, thm_name), name), i) =>
-        Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
+  OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
+    K.thy_goal
+    (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+      >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 
 end;
 

--- a/src/Pure/Isar/isar_syn.ML	Sat May 24 22:04:48 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat May 24 22:04:52 2008 +0200
@@ -232,55 +232,49 @@
 val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
 
 val _ =
-  OuterSyntax.command "definition" "constant definition" K.thy_decl
-    (P.opt_target -- constdef
-    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition_cmd args)));
+  OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
+    (constdef >> (fn args => #2 o Specification.definition_cmd args));
 
 val _ =
-  OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
-    (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
-    >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.abbreviation_cmd mode args)));
+  OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
+    (opt_mode -- (Scan.option constdecl -- P.prop)
+    >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
 
 val _ =
-  OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl
-    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
-    >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.notation_cmd true mode args)));
+  OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
+    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
+    >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
-  OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl
-    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
-    >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.notation_cmd false mode args)));
+  OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl
+    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
+    >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
 
 (* constant specifications *)
 
 val _ =
-  OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
-    (P.opt_target --
-     (Scan.optional P.fixes [] --
-      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
-    >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization_cmd x y)));
+  OuterSyntax.local_theory "axiomatization" "axiomatic constant specification" K.thy_decl
+    (Scan.optional P.fixes [] --
+      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) []
+    >> (fn (x, y) => #2 o Specification.axiomatization_cmd x y));
 
 
 (* theorems *)
 
-fun theorems kind = P.opt_target -- SpecParse.name_facts
-  >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems_cmd kind args));
+fun theorems kind =
+  SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
 
 val _ =
-  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
+  OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
 
 val _ =
-  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
+  OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
 
 val _ =
-  OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl
-    (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
-      >> (fn (loc, args) => Toplevel.local_theory loc
-          (#2 o Specification.theorems_cmd "" [(("", []), args)])));
+  OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
+    (P.and_list1 SpecParse.xthms1
+      >> (fn args => #2 o Specification.theorems_cmd "" [(("", []), flat args)]));
 
 
 (* name space entry path *)
@@ -328,16 +322,14 @@
     >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
-  OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
-    (P.opt_target -- P.position P.text
-    >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
+  OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
+    (P.position P.text >> IsarCmd.declaration);
 
 val _ =
-  OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
-    (P.opt_target --
-      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
+  OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
+    (P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
       P.position P.text -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
-    >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
+    >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
 
 
 (* translation functions *)
@@ -439,9 +431,8 @@
           (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
 
 val _ =
-  OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal
-    (P.opt_target -- P.xname >> (fn (loc, class) =>
-      Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
+  OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
+    (P.xname >> Subclass.subclass_cmd);
 
 val _ =
   OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
@@ -482,13 +473,11 @@
 (* statements *)
 
 fun gen_theorem kind =
-  OuterSyntax.command kind ("state " ^ kind) K.thy_goal
-    (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
+  OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
+    (Scan.optional (SpecParse.opt_thm_name ":" --|
       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
-      SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
-      (Toplevel.print o
-       Toplevel.local_theory_to_proof' loc
-         (Specification.theorem_cmd kind NONE (K I) a elems concl))));
+      SpecParse.general_statement >> (fn (a, (elems, concl)) =>
+        (Specification.theorem_cmd kind NONE (K I) a elems concl)));
 
 val _ = gen_theorem Thm.theoremK;
 val _ = gen_theorem Thm.lemmaK;