# HG changeset patch
# User wenzelm
# Date 1258143969 -3600
# Node ID 2582cc24bc2a94e4ae8f885d883fb10b084ef23c
# Parent  5241785055bc73117e72dec8cb13f70426480246# Parent  8bde36ec8eb1c47687c5465b4b432abfe1e818cd
merged

diff -r 5241785055bc -r 2582cc24bc2a doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Fri Nov 13 19:49:13 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Fri Nov 13 21:26:09 2009 +0100
@@ -97,13 +97,12 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML TheoryTarget.init: "string option -> theory -> local_theory"} \\[1ex]
-  @{index_ML LocalTheory.define: "string ->
+  @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex]
+  @{index_ML Local_Theory.define: "string ->
     (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory"} \\
-  @{index_ML LocalTheory.note: "string ->
-    Attrib.binding * thm list -> local_theory ->
-    (string * thm list) * local_theory"} \\
+  @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
+    local_theory -> (string * thm list) * local_theory"} \\
   \end{mldecls}
 
   \begin{description}
@@ -116,7 +115,7 @@
   with operations on expecting a regular @{text "ctxt:"}~@{ML_type
   Proof.context}.
 
-  \item @{ML TheoryTarget.init}~@{text "NONE thy"} initializes a
+  \item @{ML Theory_Target.init}~@{text "NONE thy"} initializes a
   trivial local theory from the given background theory.
   Alternatively, @{text "SOME name"} may be given to initialize a
   @{command locale} or @{command class} context (a fully-qualified
@@ -124,7 +123,7 @@
   --- normally the Isar toplevel already takes care to initialize the
   local theory context.
 
-  \item @{ML LocalTheory.define}~@{text "kind ((b, mx), (a, rhs))
+  \item @{ML Local_Theory.define}~@{text "kind ((b, mx), (a, rhs))
   lthy"} defines a local entity according to the specification that is
   given relatively to the current @{text "lthy"} context.  In
   particular the term of the RHS may refer to earlier local entities
@@ -145,13 +144,13 @@
   @{attribute simplified} are better avoided.
 
   The @{text kind} determines the theorem kind tag of the resulting
-  fact.  Typical examples are @{ML Thm.definitionK}, @{ML
-  Thm.theoremK}, or @{ML Thm.internalK}.
+  fact.  Typical examples are @{ML Thm.definitionK} or @{ML
+  Thm.theoremK}.
 
-  \item @{ML LocalTheory.note}~@{text "kind (a, ths) lthy"} is
-  analogous to @{ML LocalTheory.define}, but defines facts instead of
+  \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is
+  analogous to @{ML Local_Theory.define}, but defines facts instead of
   terms.  There is also a slightly more general variant @{ML
-  LocalTheory.notes} that defines several facts (with attribute
+  Local_Theory.notes} that defines several facts (with attribute
   expressions) simultaneously.
 
   This is essentially the internal version of the @{command lemmas}
diff -r 5241785055bc -r 2582cc24bc2a doc-src/IsarImplementation/Thy/document/Local_Theory.tex
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Fri Nov 13 19:49:13 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Fri Nov 13 21:26:09 2009 +0100
@@ -123,13 +123,12 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
-  \indexdef{}{ML}{TheoryTarget.init}\verb|TheoryTarget.init: string option -> theory -> local_theory| \\[1ex]
-  \indexdef{}{ML}{LocalTheory.define}\verb|LocalTheory.define: string ->|\isasep\isanewline%
+  \indexdef{}{ML}{Theory\_Target.init}\verb|Theory_Target.init: string option -> theory -> local_theory| \\[1ex]
+  \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: string ->|\isasep\isanewline%
 \verb|    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->|\isasep\isanewline%
 \verb|    (term * (string * thm)) * local_theory| \\
-  \indexdef{}{ML}{LocalTheory.note}\verb|LocalTheory.note: string ->|\isasep\isanewline%
-\verb|    Attrib.binding * thm list -> local_theory ->|\isasep\isanewline%
-\verb|    (string * thm list) * local_theory| \\
+  \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
+\verb|    local_theory -> (string * thm list) * local_theory| \\
   \end{mldecls}
 
   \begin{description}
@@ -141,7 +140,7 @@
   any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
   with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
 
-  \item \verb|TheoryTarget.init|~\isa{NONE\ thy} initializes a
+  \item \verb|Theory_Target.init|~\isa{NONE\ thy} initializes a
   trivial local theory from the given background theory.
   Alternatively, \isa{SOME\ name} may be given to initialize a
   \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified
@@ -149,7 +148,7 @@
   --- normally the Isar toplevel already takes care to initialize the
   local theory context.
 
-  \item \verb|LocalTheory.define|~\isa{kind\ {\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
+  \item \verb|Local_Theory.define|~\isa{kind\ {\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
   given relatively to the current \isa{lthy} context.  In
   particular the term of the RHS may refer to earlier local entities
   from the auxiliary context, or hypothetical parameters from the
@@ -169,11 +168,11 @@
   \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}} are better avoided.
 
   The \isa{kind} determines the theorem kind tag of the resulting
-  fact.  Typical examples are \verb|Thm.definitionK|, \verb|Thm.theoremK|, or \verb|Thm.internalK|.
+  fact.  Typical examples are \verb|Thm.definitionK| or \verb|Thm.theoremK|.
 
-  \item \verb|LocalTheory.note|~\isa{kind\ {\isacharparenleft}a{\isacharcomma}\ ths{\isacharparenright}\ lthy} is
-  analogous to \verb|LocalTheory.define|, but defines facts instead of
-  terms.  There is also a slightly more general variant \verb|LocalTheory.notes| that defines several facts (with attribute
+  \item \verb|Local_Theory.note|~\isa{{\isacharparenleft}a{\isacharcomma}\ ths{\isacharparenright}\ lthy} is
+  analogous to \verb|Local_Theory.define|, but defines facts instead of
+  terms.  There is also a slightly more general variant \verb|Local_Theory.notes| that defines several facts (with attribute
   expressions) simultaneously.
 
   This is essentially the internal version of the \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}
diff -r 5241785055bc -r 2582cc24bc2a src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Fri Nov 13 21:26:09 2009 +0100
@@ -195,7 +195,7 @@
 begin
 
 thm lor_def
-(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *)
+(* Can we get rid the the additional hypothesis, caused by Local_Theory.notes? *)
 
 lemma "x || y = --(-- x && --y)"
   by (unfold lor_def) (rule refl)
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -38,7 +38,7 @@
   | SOME vc =>
       let
         fun store thm = Boogie_VCs.discharge (name, thm)
-        fun after_qed [[thm]] = LocalTheory.theory (store thm)
+        fun after_qed [[thm]] = Local_Theory.theory (store thm)
           | after_qed _ = I
       in
         lthy
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -569,9 +569,8 @@
       thy3
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = false, verbose = false, kind = "",
-           alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
-           skip_mono = true, fork_mono = false}
+          {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
+           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
           [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
@@ -1513,9 +1512,8 @@
       thy10
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = #quiet config, verbose = false, kind = "",
-           alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
-           skip_mono = true, fork_mono = false}
+          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
+           coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
           (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -561,20 +561,19 @@
             (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
             [ind_case_names, Rule_Cases.consumes 1]);
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
+        val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
           ((rec_qualified (Binding.name "strong_induct"),
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
-          ctxt;
+            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
         val strong_inducts =
-          Project_Rule.projects ctxt (1 upto length names) strong_induct'
+          Project_Rule.projects ctxt (1 upto length names) strong_induct';
       in
         ctxt' |>
-        LocalTheory.note ""
+        Local_Theory.note
           ((rec_qualified (Binding.name "strong_inducts"),
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (Rule_Cases.consumes 1))]),
            strong_inducts) |> snd |>
-        LocalTheory.notes "" (map (fn ((name, elim), (_, cases)) =>
+        Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
               [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
                Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
@@ -664,7 +663,7 @@
       end) atoms
   in
     ctxt |>
-    LocalTheory.notes "" (map (fn (name, ths) =>
+    Local_Theory.notes (map (fn (name, ths) =>
         ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
           [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
       (names ~~ transp thss)) |> snd
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -466,15 +466,14 @@
             NONE => (rec_qualified (Binding.name "strong_induct"),
                      rec_qualified (Binding.name "strong_inducts"))
           | SOME s => (Binding.name s, Binding.name (s ^ "s"));
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
+        val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
           ((induct_name,
-            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
-          ctxt;
+            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
         val strong_inducts =
           Project_Rule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
-        LocalTheory.note ""
+        Local_Theory.note
           ((inducts_name,
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (Rule_Cases.consumes 1))]),
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -280,9 +280,8 @@
       else primrec_err ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
     val (defs_thms, lthy') = lthy |>
-      set_group ? LocalTheory.set_group (serial ()) |>
-      fold_map (apfst (snd o snd) oo
-        LocalTheory.define Thm.definitionK o fst) defs';
+      set_group ? Local_Theory.set_group (serial ()) |>
+      fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
     val qualify = Binding.qualify false
       (space_implode "_" (map (Long_Name.base_name o #1) defs));
     val names_atts' = map (apfst qualify) names_atts;
@@ -367,11 +366,11 @@
       (fn thss => fn goal_ctxt =>
          let
            val simps = ProofContext.export goal_ctxt lthy' (flat thss);
-           val (simps', lthy'') = fold_map (LocalTheory.note "")
-             (names_atts' ~~ map single simps) lthy'
+           val (simps', lthy'') =
+            fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy';
          in
            lthy''
-           |> LocalTheory.note "" ((qualify (Binding.name "simps"),
+           |> Local_Theory.note ((qualify (Binding.name "simps"),
                 map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
                 maps snd simps')
            |> snd
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -155,13 +155,13 @@
   thy 
   |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
   |> snd
-  |> LocalTheory.exit;
+  |> Local_Theory.exit;
 
 fun add_locale_cmd name expr elems thy =
   thy 
   |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
   |> snd
-  |> LocalTheory.exit;
+  |> Local_Theory.exit;
 
 type statespace_info =
  {args: (string * sort) list, (* type arguments *)
@@ -350,8 +350,8 @@
 fun add_declaration name decl thy =
   thy
   |> Theory_Target.init name
-  |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
-  |> LocalTheory.exit_global;
+  |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
+  |> Local_Theory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
   let
@@ -430,7 +430,7 @@
           let
             fun upd (n,v) =
               let
-                val nT = ProofContext.infer_type (LocalTheory.target_of lthy) n
+                val nT = ProofContext.infer_type (Local_Theory.target_of lthy) n
               in Context.proof_map
                   (update_declinfo (Morphism.term phi (Free (n,nT)),v))
               end;
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -156,9 +156,8 @@
       thy0
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = #quiet config, verbose = false, kind = "",
-            alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
-            skip_mono = true, fork_mono = false}
+          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
+            coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
           (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -175,9 +175,8 @@
       thy1
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = #quiet config, verbose = false, kind = "",
-           alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
-           skip_mono = true, fork_mono = false}
+          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
+           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
           (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
       ||> Sign.restore_naming thy1
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -153,11 +153,11 @@
 fun gen_fun add config fixes statements int lthy =
   let val group = serial () in
     lthy
-      |> LocalTheory.set_group group
+      |> Local_Theory.set_group group
       |> add fixes statements config
       |> by_pat_completeness_auto int
-      |> LocalTheory.restore
-      |> LocalTheory.set_group group
+      |> Local_Theory.restore
+      |> Local_Theory.set_group group
       |> termination_by (Function_Common.get_termination_prover lthy) int
   end;
 
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -43,9 +43,6 @@
     [Simplifier.simp_add,
      Nitpick_Psimps.add]
 
-fun note_theorem ((binding, atts), ths) =
-  LocalTheory.note "" ((binding, atts), ths)
-
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
 fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
@@ -55,13 +52,14 @@
                    |> map (apfst (apfst extra_qualify))
 
       val (saved_spec_simps, lthy) =
-        fold_map (LocalTheory.note "") spec lthy
+        fold_map Local_Theory.note spec lthy
 
       val saved_simps = maps snd saved_spec_simps
       val simps_by_f = sort saved_simps
 
       fun add_for_f fname simps =
-        note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
+        Local_Theory.note
+          ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
         #> snd
     in
       (saved_simps,
@@ -100,14 +98,14 @@
             |> addsmps (conceal_partial o Binding.qualify false "partial")
                  "psimps" conceal_partial psimp_attribs psimps
             ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
-            ||>> note_theorem ((conceal_partial (qualify "pinduct"),
+            ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
                    [Attrib.internal (K (Rule_Cases.case_names cnames)),
                     Attrib.internal (K (Rule_Cases.consumes 1)),
                     Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
-            ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination])
-            ||> (snd o note_theorem ((qualify "cases",
+            ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
+            ||> (snd o Local_Theory.note ((qualify "cases",
                    [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
-            ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
+            ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
 
           val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
                                       pinducts=snd pinducts', termination=termination',
@@ -117,11 +115,11 @@
             else Specification.print_consts lthy (K false) (map fst fixes)
         in
           lthy
-          |> LocalTheory.declaration false (add_function_data o morph_function_data cdata)
+          |> Local_Theory.declaration false (add_function_data o morph_function_data cdata)
         end
     in
       lthy
-        |> is_external ? LocalTheory.set_group (serial ())
+        |> is_external ? Local_Theory.set_group (serial ())
         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
     end
@@ -155,7 +153,7 @@
           in
             lthy
             |> add_simps I "simps" I simp_attribs tsimps |> snd
-            |> note_theorem
+            |> Local_Theory.note
                ((qualify "induct",
                  [Attrib.internal (K (Rule_Cases.case_names case_names))]),
                 tinduct) |> snd
@@ -177,12 +175,12 @@
 
 fun termination term_opt lthy =
   lthy
-  |> LocalTheory.set_group (serial ())
+  |> Local_Theory.set_group (serial ())
   |> termination_proof term_opt;
 
 fun termination_cmd term_opt lthy =
   lthy
-  |> LocalTheory.set_group (serial ())
+  |> Local_Theory.set_group (serial ())
   |> termination_proof_cmd term_opt;
 
 
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -456,11 +456,10 @@
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
       lthy
-      |> LocalTheory.conceal
+      |> Local_Theory.conceal
       |> Inductive.add_inductive_i
           {quiet_mode = true,
             verbose = ! trace,
-            kind = "",
             alt_name = Binding.empty,
             coind = false,
             no_elim = false,
@@ -471,7 +470,7 @@
           [] (* no parameters *)
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
           [] (* no special monos *)
-      ||> LocalTheory.restore_naming lthy
+      ||> Local_Theory.restore_naming lthy
 
     val cert = cterm_of (ProofContext.theory_of lthy)
     fun requantify orig_intro thm =
@@ -519,7 +518,7 @@
         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
       |> Syntax.check_term lthy
   in
-    LocalTheory.define ""
+    Local_Theory.define ""
       ((Binding.name (function_name fname), mixfix),
         ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
   end
@@ -929,7 +928,7 @@
           PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
       val (_, lthy) =
-          LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
+          Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
 
       val newthy = ProofContext.theory_of lthy
       val clauses = map (transfer_clause_ctx newthy) clauses
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -146,7 +146,7 @@
       fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
           let
             val ((f, (_, f_defthm)), lthy') =
-              LocalTheory.define ""
+              Local_Theory.define ""
                 ((Binding.name fname, mixfix),
                   ((Binding.conceal (Binding.name (fname ^ "_def")), []),
                   Term.subst_bound (fsum, f_def))) lthy
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -130,7 +130,7 @@
     fun define_overloaded (def_name, eq) lthy =
       let
         val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
-        val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
+        val ((_, (_, thm)), lthy') = lthy |> Local_Theory.define Thm.definitionK
           ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
@@ -149,7 +149,7 @@
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
       ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-      ||> LocalTheory.exit_global;
+      ||> Local_Theory.exit_global;
 
     val ctxt = ProofContext.init thy';
 
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -137,8 +137,8 @@
   in
     if (is_inductify options) then
       let
-        val lthy' = LocalTheory.theory (preprocess options const) lthy
-          |> LocalTheory.checkpoint
+        val lthy' = Local_Theory.theory (preprocess options const) lthy
+          |> Local_Theory.checkpoint
         val const =
           case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
             SOME c => c
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -2411,9 +2411,9 @@
   let
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
-    val lthy' = LocalTheory.theory (PredData.map
+    val lthy' = Local_Theory.theory (PredData.map
         (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
-      |> LocalTheory.checkpoint
+      |> Local_Theory.checkpoint
     val thy' = ProofContext.theory_of lthy'
     val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
     fun mk_cases const =
@@ -2437,7 +2437,7 @@
         val global_thms = ProofContext.export goal_ctxt
           (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
       in
-        goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
+        goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
           (if is_random options then
             (add_equations options [const] #>
             add_quickcheck_equations options [const])
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -355,9 +355,8 @@
               thy
               |> Sign.map_naming Name_Space.conceal
               |> Inductive.add_inductive_global (serial ())
-                {quiet_mode = false, verbose = false, kind = "",
-                  alt_name = Binding.empty, coind = false, no_elim = false,
-                  no_ind = false, skip_mono = false, fork_mono = false}
+                {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
+                  no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
                 (map (fn (s, T) =>
                   ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
                 pnames
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -39,8 +39,8 @@
   val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
     thm list list * local_theory
   type inductive_flags =
-    {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
-     coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
+    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
+      no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
   val add_inductive_i:
     inductive_flags -> ((binding * typ) * mixfix) list ->
     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
@@ -71,7 +71,7 @@
     term list -> (Attrib.binding * term) list -> thm list ->
     term list -> (binding * mixfix) list ->
     local_theory -> inductive_result * local_theory
-  val declare_rules: string -> binding -> bool -> bool -> string list ->
+  val declare_rules: binding -> bool -> bool -> string list ->
     thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
     thm -> local_theory -> thm list * thm list * thm * local_theory
   val add_ind_def: add_ind_def
@@ -469,7 +469,7 @@
     val facts = args |> map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
         map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
-  in lthy |> LocalTheory.notes "" facts |>> map snd end;
+  in lthy |> Local_Theory.notes facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
@@ -509,7 +509,8 @@
 
     fun mk_ind_prem r =
       let
-        fun subst s = (case dest_predicate cs params s of
+        fun subst s =
+          (case dest_predicate cs params s of
             SOME (_, i, ys, (_, Ts)) =>
               let
                 val k = length Ts;
@@ -520,10 +521,11 @@
                   HOLogic.mk_binop inductive_conj_name
                     (list_comb (incr_boundvars k s, bs), P))
               in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
-          | NONE => (case s of
-              (t $ u) => (fst (subst t) $ fst (subst u), NONE)
-            | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
-            | _ => (s, NONE)));
+          | NONE =>
+              (case s of
+                (t $ u) => (fst (subst t) $ fst (subst u), NONE)
+              | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
+              | _ => (s, NONE)));
 
         fun mk_prem s prems =
           (case subst s of
@@ -618,16 +620,17 @@
         SOME (_, i, ts, (Ts, Us)) =>
           let
             val l = length Us;
-            val zs = map Bound (l - 1 downto 0)
+            val zs = map Bound (l - 1 downto 0);
           in
             list_abs (map (pair "z") Us, list_comb (p,
               make_bool_args' bs i @ make_args argTs
                 ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
           end
-      | NONE => (case t of
-          t1 $ t2 => subst t1 $ subst t2
-        | Abs (x, T, u) => Abs (x, T, subst u)
-        | _ => t));
+      | NONE =>
+          (case t of
+            t1 $ t2 => subst t1 $ subst t2
+          | Abs (x, T, u) => Abs (x, T, subst u)
+          | _ => t));
 
     (* transform an introduction rule into a conjunction  *)
     (*   [| p_i t; ... |] ==> p_j u                       *)
@@ -662,13 +665,13 @@
       else alt_name;
 
     val ((rec_const, (_, fp_def)), lthy') = lthy
-      |> LocalTheory.conceal
-      |> LocalTheory.define ""
+      |> Local_Theory.conceal
+      |> Local_Theory.define ""
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
          fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
-      ||> LocalTheory.restore_naming lthy;
+      ||> Local_Theory.restore_naming lthy;
     val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
       (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params)));
     val specs =
@@ -685,21 +688,21 @@
                 make_args argTs (xs ~~ Ts)))))
           end) (cnames_syn ~~ cs);
     val (consts_defs, lthy'') = lthy'
-      |> LocalTheory.conceal
-      |> fold_map (LocalTheory.define "") specs
-      ||> LocalTheory.restore_naming lthy';
+      |> Local_Theory.conceal
+      |> fold_map (Local_Theory.define "") specs
+      ||> Local_Theory.restore_naming lthy';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
     val ((_, [mono']), lthy''') =
-      LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
 
   in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
   end;
 
-fun declare_rules kind rec_binding coind no_ind cnames
-      intrs intr_bindings intr_atts elims raw_induct lthy =
+fun declare_rules rec_binding coind no_ind cnames
+    intrs intr_bindings intr_atts elims raw_induct lthy =
   let
     val rec_name = Binding.name_of rec_binding;
     fun rec_qualified qualified = Binding.qualify qualified rec_name;
@@ -716,7 +719,7 @@
 
     val (intrs', lthy1) =
       lthy |>
-      LocalTheory.notes kind
+      Local_Theory.notes
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
           map (fn th => [([th],
            [Attrib.internal (K (Context_Rules.intro_query NONE)),
@@ -724,16 +727,16 @@
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), lthy2) =
       lthy1 |>
-      LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
+      Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
-        LocalTheory.note kind
+        Local_Theory.note
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
             [Attrib.internal (K (Rule_Cases.case_names cases)),
              Attrib.internal (K (Rule_Cases.consumes 1)),
              Attrib.internal (K (Induct.cases_pred name)),
              Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
-      LocalTheory.note kind
+      Local_Theory.note
         ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
           map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
@@ -742,7 +745,7 @@
       else
         let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
           lthy2 |>
-          LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
+          Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
             inducts |> map (fn (name, th) => ([th],
               [Attrib.internal (K ind_case_names),
                Attrib.internal (K (Rule_Cases.consumes 1)),
@@ -751,8 +754,8 @@
   in (intrs', elims', induct', lthy3) end;
 
 type inductive_flags =
-  {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
-   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
+  {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
+    no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
 
 type add_ind_def =
   inductive_flags ->
@@ -760,8 +763,7 @@
   term list -> (binding * mixfix) list ->
   local_theory -> inductive_result * local_theory;
 
-fun add_ind_def
-    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn lthy =
   let
     val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -769,7 +771,7 @@
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
-    val cnames = map (LocalTheory.full_name lthy o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn;  (* FIXME *)
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule lthy cs params) intros));
 
@@ -797,7 +799,7 @@
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
            rec_preds_defs lthy1);
 
-    val (intrs', elims', induct, lthy2) = declare_rules kind rec_name coind no_ind
+    val (intrs', elims', induct, lthy2) = declare_rules rec_name coind no_ind
       cnames intrs intr_names intr_atts elims raw_induct lthy1;
 
     val result =
@@ -808,7 +810,7 @@
        induct = induct};
 
     val lthy3 = lthy2
-      |> LocalTheory.declaration false (fn phi =>
+      |> Local_Theory.declaration false (fn phi =>
         let val result' = morph_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
   in (result, lthy3) end;
@@ -817,7 +819,7 @@
 (* external interfaces *)
 
 fun gen_add_inductive_i mk_def
-    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
+    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
     cnames_syn pnames spec monos lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -870,7 +872,7 @@
   in
     lthy
     |> mk_def flags cs intros monos ps preds
-    ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs
+    ||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
   end;
 
 fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
@@ -880,12 +882,11 @@
       |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
     val (cs, ps) = chop (length cnames_syn) vars;
     val monos = Attrib.eval_thms lthy raw_monos;
-    val flags = {quiet_mode = false, verbose = verbose, kind = "",
-      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
-      skip_mono = false, fork_mono = not int};
+    val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
+      coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
   in
     lthy
-    |> LocalTheory.set_group (serial ())
+    |> Local_Theory.set_group (serial ())
     |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
   end;
 
@@ -897,9 +898,9 @@
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
       |> Theory_Target.init NONE
-      |> LocalTheory.set_group group
+      |> Local_Theory.set_group group
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
-      |> LocalTheory.exit;
+      |> Local_Theory.exit;
     val info = #2 (the_inductive ctxt' name);
   in (info, ProofContext.theory_of ctxt') end;
 
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -14,7 +14,7 @@
 structure InductiveRealizer : INDUCTIVE_REALIZER =
 struct
 
-(* FIXME: LocalTheory.note should return theorems with proper names! *)  (* FIXME ?? *)
+(* FIXME: Local_Theory.note should return theorems with proper names! *)  (* FIXME ?? *)
 fun name_of_thm thm =
   (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
       [Thm.proof_of thm] [] of
@@ -351,8 +351,8 @@
 
     val (ind_info, thy3') = thy2 |>
       Inductive.add_inductive_global (serial ())
-        {quiet_mode = false, verbose = false, kind = "", alt_name = Binding.empty,
-          coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
+        {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
+          no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -224,7 +224,7 @@
   map (fn (x, ps) =>
     let
       val U = HOLogic.dest_setT (fastype_of x);
-      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
+      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
     in
       (cterm_of thy x,
        cterm_of thy (HOLogic.Collect_const U $
@@ -405,7 +405,7 @@
 (**** definition of inductive sets ****)
 
 fun add_ind_set_def
-    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
+    {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -477,20 +477,20 @@
     val monos' = map (to_pred [] (Context.Proof lthy)) monos;
     val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
       Inductive.add_ind_def
-        {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
+        {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
           coind = coind, no_elim = no_elim, no_ind = no_ind,
           skip_mono = skip_mono, fork_mono = fork_mono}
         cs' intros' monos' params1 cnames_syn' lthy;
 
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
-      |> LocalTheory.conceal  (* FIXME ?? *)
-      |> fold_map (LocalTheory.define "")
+      |> Local_Theory.conceal  (* FIXME ?? *)
+      |> fold_map (Local_Theory.define "")
         (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
            (cnames_syn ~~ cs_info ~~ preds))
-      ||> LocalTheory.restore_naming lthy1;
+      ||> Local_Theory.restore_naming lthy1;
 
     (* prove theorems for converting predicate to set notation *)
     val lthy3 = fold
@@ -505,7 +505,7 @@
             (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
               [def, mem_Collect_eq, split_conv]) 1))
         in
-          lthy |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
+          lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal (K pred_set_conv_att)]),
               [conv_thm]) |> snd
         end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
@@ -515,11 +515,11 @@
       if Binding.is_empty alt_name then
         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
-    val cnames = map (LocalTheory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     val (intrs', elims', induct, lthy4) =
-      Inductive.declare_rules kind rec_name coind no_ind cnames
+      Inductive.declare_rules rec_name coind no_ind cnames
         (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
         (map (fn th => (to_set [] (Context.Proof lthy3) th,
            map fst (fst (Rule_Cases.get th)))) elims)
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -259,7 +259,7 @@
     val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   in
     lthy
-    |> fold_map (LocalTheory.define Thm.definitionK) defs
+    |> fold_map (Local_Theory.define Thm.definitionK) defs
     |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
   end;
 
@@ -275,10 +275,10 @@
         map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
   in
     lthy
-    |> set_group ? LocalTheory.set_group (serial ())
+    |> set_group ? Local_Theory.set_group (serial ())
     |> add_primrec_simple fixes (map snd spec)
-    |-> (fn (prefix, simps) => fold_map (LocalTheory.note "") (attr_bindings prefix ~~ simps)
-      #-> (fn simps' => LocalTheory.note "" (simp_attr_binding prefix, maps snd simps')))
+    |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
+      #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')))
     |>> snd
   end;
 
@@ -294,14 +294,14 @@
     val lthy = Theory_Target.init NONE thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
-  in (simps', LocalTheory.exit_global lthy') end;
+  in (simps', Local_Theory.exit_global lthy') end;
 
 fun add_primrec_overloaded ops fixes specs thy =
   let
     val lthy = Theory_Target.overloading ops thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
-  in (simps', LocalTheory.exit_global lthy') end;
+  in (simps', Local_Theory.exit_global lthy') end;
 
 
 (* outer syntax *)
diff -r 5241785055bc -r 2582cc24bc2a src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -190,7 +190,7 @@
       in
         lthy
         |> random_aux_primrec aux_eq'
-        ||>> fold_map (LocalTheory.define Thm.definitionK) proj_defs
+        ||>> fold_map (Local_Theory.define Thm.definitionK) proj_defs
         |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
       end;
 
@@ -214,7 +214,7 @@
     lthy
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> (fn proto_simps => prove_simps proto_simps)
-    |-> (fn simps => LocalTheory.note ""
+    |-> (fn simps => Local_Theory.note
       ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
           [Simplifier.simp_add, Nitpick_Simps.add]), simps))
     |> snd
diff -r 5241785055bc -r 2582cc24bc2a src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -209,7 +209,7 @@
       | defs (l::[]) r = [one_def l r]
       | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
     val fixdefs = defs lhss fixpoint;
-    val define_all = fold_map (LocalTheory.define Thm.definitionK);
+    val define_all = fold_map (Local_Theory.define Thm.definitionK);
     val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
       |> define_all (map (apfst fst) fixes ~~ fixdefs);
     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
@@ -242,7 +242,7 @@
         ((thm_name, [src]), [thm])
       end;
     val (thmss, lthy'') = lthy'
-      |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms);
+      |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms);
   in
     (lthy'', names, fixdef_thms, map snd unfold_thms)
   end;
@@ -464,7 +464,7 @@
       val simps2 : (Attrib.binding * thm list) list =
         map (apsnd (fn thm => [thm])) (flat simps);
       val (_, lthy'') = lthy'
-        |> fold_map (LocalTheory.note "") (simps1 @ simps2);
+        |> fold_map Local_Theory.note (simps1 @ simps2);
     in
       lthy''
     end
diff -r 5241785055bc -r 2582cc24bc2a src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -201,7 +201,7 @@
     val thy5 = lthy4
       |> Class.prove_instantiation_instance
           (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
-      |> LocalTheory.exit_global;
+      |> Local_Theory.exit_global;
   in ((info, below_definition), thy5) end;
 
 fun prepare_cpodef
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/class.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -281,7 +281,7 @@
   in
     thy
     |> Expression.add_locale bname Binding.empty supexpr elems
-    |> snd |> LocalTheory.exit_global
+    |> snd |> Local_Theory.exit_global
     |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -405,9 +405,9 @@
 
 fun mk_instantiation (arities, params) =
   Instantiation { arities = arities, params = params };
-fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
+fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy)
  of Instantiation data => data;
-fun map_instantiation f = (LocalTheory.target o Instantiation.map)
+fun map_instantiation f = (Local_Theory.target o Instantiation.map)
   (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
 
 fun the_instantiation lthy = case get_instantiation lthy
@@ -526,14 +526,14 @@
 
 fun confirm_declaration b = (map_instantiation o apsnd)
   (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
-  #> LocalTheory.target synchronize_inst_syntax
+  #> Local_Theory.target synchronize_inst_syntax
 
 fun gen_instantiation_instance do_proof after_qed lthy =
   let
     val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
     val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
     fun after_qed' results =
-      LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
+      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
       #> after_qed;
   in
     lthy
@@ -548,7 +548,7 @@
     (fn {context, ...} => tac context)) ts) lthy) I;
 
 fun prove_instantiation_exit tac = prove_instantiation_instance tac
-  #> LocalTheory.exit_global;
+  #> Local_Theory.exit_global;
 
 fun prove_instantiation_exit_result f tac x lthy =
   let
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -775,7 +775,7 @@
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
       |> Theory_Target.init (SOME name)
-      |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
+      |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
 
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -181,7 +181,7 @@
 fun declaration pervasive (txt, pos) =
   txt |> ML_Context.expression pos
     "val declaration: Morphism.declaration"
-    ("Context.map_proof (LocalTheory.declaration " ^ Bool.toString pervasive ^ " declaration)")
+    ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
   |> Context.proof_map;
 
 
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -288,7 +288,7 @@
 (* use ML text *)
 
 fun propagate_env (context as Context.Proof lthy) =
-      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
+      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
   | propagate_env context = context;
 
 fun propagate_env_prf prf = Proof.map_contexts
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -33,8 +33,10 @@
     (term * term) * local_theory
   val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
-  val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
-  val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+  val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
+  val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    local_theory -> (string * thm list) list * local_theory
+  val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
   val type_syntax: bool -> declaration -> local_theory -> local_theory
   val term_syntax: bool -> declaration -> local_theory -> local_theory
@@ -49,7 +51,7 @@
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
 end;
 
-structure LocalTheory: LOCAL_THEORY =
+structure Local_Theory: LOCAL_THEORY =
 struct
 
 (** local theory data **)
@@ -186,12 +188,13 @@
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
 val define = apsnd checkpoint ooo operation2 #define;
-val notes = apsnd checkpoint ooo operation2 #notes;
+val notes_kind = apsnd checkpoint ooo operation2 #notes;
 val type_syntax = checkpoint ooo operation2 #type_syntax;
 val term_syntax = checkpoint ooo operation2 #term_syntax;
 val declaration = checkpoint ooo operation2 #declaration;
 
-fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
+val notes = notes_kind "";
+fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/overloading.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -126,8 +126,8 @@
   fun init _ = [];
 );
 
-val get_overloading = OverloadingData.get o LocalTheory.target_of;
-val map_overloading = LocalTheory.target o OverloadingData.map;
+val get_overloading = OverloadingData.get o Local_Theory.target_of;
+val map_overloading = Local_Theory.target o OverloadingData.map;
 
 fun operation lthy b = get_overloading lthy
   |> get_first (fn ((c, _), (v, checked)) =>
@@ -169,7 +169,7 @@
   (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
 
 fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
-  #> LocalTheory.target synchronize_syntax
+  #> Local_Theory.target synchronize_syntax
 
 fun conclude lthy =
   let
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -41,7 +41,7 @@
 val get = Item_Net.content o Rules.get o Context.Proof;
 val get_global = Item_Net.content o Rules.get o Context.Theory;
 
-fun add class (ts, ths) = LocalTheory.declaration true
+fun add class (ts, ths) = Local_Theory.declaration true
   (fn phi =>
     let
       val ts' = map (Morphism.term phi) ts;
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -202,18 +202,18 @@
           in (b, mx) end);
     val name = Thm.def_binding_optional b raw_name;
     val ((lhs, (_, raw_th)), lthy2) = lthy
-      |> LocalTheory.define Thm.definitionK
+      |> Local_Theory.define Thm.definitionK
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
 
     val th = prove lthy2 raw_th;
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
 
-    val ((def_name, [th']), lthy4) = lthy3
-      |> LocalTheory.note Thm.definitionK
-        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
-            Code.add_default_eqn_attrib :: atts), [th]);
+    val ([(def_name, [th'])], lthy4) = lthy3
+      |> Local_Theory.notes_kind Thm.definitionK
+        [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
+            Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
-    val lhs' = Morphism.term (LocalTheory.target_morphism lthy4) lhs;
+    val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
     val _ =
       if not do_print then ()
       else print_consts lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
@@ -243,7 +243,7 @@
           in (b, mx) end);
     val lthy' = lthy
       |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
-      |> LocalTheory.abbrev mode (var, rhs) |> snd
+      |> Local_Theory.abbrev mode (var, rhs) |> snd
       |> ProofContext.restore_syntax_mode lthy;
 
     val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
@@ -256,7 +256,7 @@
 (* notation *)
 
 fun gen_notation prep_const add mode args lthy =
-  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
+  lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
 
 val notation = gen_notation (K I);
 val notation_cmd = gen_notation ProofContext.read_const;
@@ -270,7 +270,7 @@
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
       ((name, map attrib atts),
         bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
-    val (res, lthy') = lthy |> LocalTheory.notes kind facts;
+    val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts;
     val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
   in (res, lthy') end;
 
@@ -345,7 +345,7 @@
 fun gen_theorem prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
   let
-    val _ = LocalTheory.affirm lthy;
+    val _ = Local_Theory.affirm lthy;
     val thy = ProofContext.theory_of lthy;
 
     val attrib = prep_att thy;
@@ -359,14 +359,15 @@
         burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
       in
         lthy
-        |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
+        |> Local_Theory.notes_kind kind
+          (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
           if Binding.is_empty name andalso null atts then
             (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') = lthy'
-                |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
+                |> Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
               val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
             in lthy'' end)
         |> after_qed results'
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -77,14 +77,14 @@
 
 fun direct_decl decl =
   let val decl0 = Morphism.form decl in
-    LocalTheory.theory (Context.theory_map decl0) #>
-    LocalTheory.target (Context.proof_map decl0)
+    Local_Theory.theory (Context.theory_map decl0) #>
+    Local_Theory.target (Context.proof_map decl0)
   end;
 
 fun target_decl add (Target {target, ...}) pervasive decl lthy =
   let
-    val global_decl = Morphism.transform (LocalTheory.global_morphism lthy) decl;
-    val target_decl = Morphism.transform (LocalTheory.target_morphism lthy) decl;
+    val global_decl = Morphism.transform (Local_Theory.global_morphism lthy) decl;
+    val target_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
   in
     if target = "" then
       lthy
@@ -92,7 +92,7 @@
     else
       lthy
       |> pervasive ? direct_decl global_decl
-      |> LocalTheory.target (add target target_decl)
+      |> Local_Theory.target (add target target_decl)
   end;
 
 in
@@ -104,8 +104,8 @@
 end;
 
 fun class_target (Target {target, ...}) f =
-  LocalTheory.raw_theory f #>
-  LocalTheory.target (Class_Target.refresh_syntax target);
+  Local_Theory.raw_theory f #>
+  Local_Theory.target (Class_Target.refresh_syntax target);
 
 
 (* notes *)
@@ -161,19 +161,19 @@
     val thy = ProofContext.theory_of lthy;
     val facts' = facts
       |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
-          (LocalTheory.full_name lthy (fst a))) bs))
+          (Local_Theory.full_name lthy (fst a))) bs))
       |> PureThy.map_facts (import_export_proof lthy);
     val local_facts = PureThy.map_facts #1 facts'
       |> Attrib.map_facts (Attrib.attribute_i thy);
     val target_facts = PureThy.map_facts #1 facts'
-      |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy));
+      |> is_locale ? Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy));
     val global_facts = PureThy.map_facts #2 facts'
       |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
   in
     lthy
-    |> LocalTheory.theory (PureThy.note_thmss kind global_facts #> snd)
-    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
-    |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
+    |> Local_Theory.theory (PureThy.note_thmss kind global_facts #> snd)
+    |> not is_locale ? Local_Theory.target (ProofContext.note_thmss kind global_facts #> snd)
+    |> is_locale ? Local_Theory.target (Locale.add_thmss target kind target_facts)
     |> ProofContext.note_thmss kind local_facts
   end;
 
@@ -212,22 +212,22 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
+    val xs = filter depends (#1 (ProofContext.inferred_fixes (Local_Theory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val (const, lthy') = lthy |>
       (case Class_Target.instantiation_param lthy b of
         SOME c' =>
           if mx3 <> NoSyn then syntax_error c'
-          else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
+          else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
             ##> Class_Target.confirm_declaration b
         | NONE =>
             (case Overloading.operation lthy b of
               SOME (c', _) =>
                 if mx3 <> NoSyn then syntax_error c'
-                else LocalTheory.theory_result (Overloading.declare (c', U))
+                else Local_Theory.theory_result (Overloading.declare (c', U))
                   ##> Overloading.confirm b
-            | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
+            | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
@@ -242,7 +242,7 @@
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   let
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
-    val target_ctxt = LocalTheory.target_of lthy;
+    val target_ctxt = Local_Theory.target_of lthy;
 
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val t' = Assumption.export_term lthy target_ctxt t;
@@ -253,14 +253,14 @@
   in
     lthy |>
      (if is_locale then
-        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
+        Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta false (locale_const ta prmode ((b, mx2), lhs')) #>
             is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
           end)
       else
-        LocalTheory.theory
+        Local_Theory.theory
           (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
     |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
@@ -278,7 +278,7 @@
     val name' = Thm.def_binding_optional b name;
     val (rhs', rhs_conv) =
       LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
-    val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
+    val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
     val T = Term.fastype_of rhs;
 
     (*const*)
@@ -287,7 +287,7 @@
 
     (*def*)
     val (global_def, lthy3) = lthy2
-      |> LocalTheory.theory_result
+      |> Local_Theory.theory_result
         (case Overloading.operation lthy b of
           SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
         | NONE =>
@@ -310,7 +310,8 @@
 local
 
 fun init_target _ NONE = global_target
-  | init_target thy (SOME target) = if Locale.defined thy (Locale.intern thy target)
+  | init_target thy (SOME target) =
+      if Locale.defined thy (Locale.intern thy target)
       then make_target target true (Class_Target.is_class thy target) ([], [], []) []
       else error ("No such locale: " ^ quote target);
 
@@ -323,7 +324,7 @@
 
 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   Data.put ta #>
-  LocalTheory.init (Long_Name.base_name target)
+  Local_Theory.init (Long_Name.base_name target)
    {pretty = pretty ta,
     abbrev = abbrev ta,
     define = define ta,
@@ -332,7 +333,7 @@
     term_syntax = term_syntax ta,
     declaration = declaration ta,
     reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
-    exit = LocalTheory.target_of o
+    exit = Local_Theory.target_of o
       (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
        else if not (null overloading) then Overloading.conclude
        else I)}
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -105,16 +105,16 @@
 type generic_theory = Context.generic;    (*theory or local_theory*)
 
 val loc_init = Theory_Target.context;
-val loc_exit = LocalTheory.exit_global;
+val loc_exit = Local_Theory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy
   | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
 
 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
-  | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore
+  | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
   | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
-      Context.Proof (LocalTheory.reinit (LocalTheory.raw_theory (K (loc_exit lthy')) lthy));
+      Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy));
 
 
 (* datatype node *)
@@ -193,7 +193,7 @@
 
 (* print state *)
 
-val pretty_context = LocalTheory.pretty o Context.cases (Theory_Target.init NONE) I;
+val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
 
 fun print_state_context state =
   (case try node_of state of
@@ -259,7 +259,7 @@
   | stale_error some = some;
 
 fun map_theory f (Theory (gthy, ctxt)) =
-      Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, ctxt)
+      Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt)
   | map_theory _ node = node;
 
 in
diff -r 5241785055bc -r 2582cc24bc2a src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/Pure/simplifier.ML	Fri Nov 13 21:26:09 2009 +0100
@@ -177,7 +177,7 @@
 fun gen_simproc prep {name, lhss, proc, identifier} lthy =
   let
     val b = Binding.name name;
-    val naming = LocalTheory.naming_of lthy;
+    val naming = Local_Theory.naming_of lthy;
     val simproc = make_simproc
       {name = Name_Space.full_name naming b,
        lhss =
@@ -191,7 +191,7 @@
        proc = proc,
        identifier = identifier};
   in
-    lthy |> LocalTheory.declaration false (fn phi =>
+    lthy |> Local_Theory.declaration false (fn phi =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;
@@ -335,7 +335,8 @@
     "declaration of Simplifier rewrite rule" #>
   Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
     "declaration of Simplifier congruence rule" #>
-  Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
+  Attrib.setup (Binding.name "simproc") simproc_att
+    "declaration of simplification procedures" #>
   Attrib.setup (Binding.name "simplified") simplified "simplified rule"));