modernized structure Local_Theory;
authorwenzelm
Fri Nov 13 21:11:15 2009 +0100 (2009-11-13 ago)
changeset 336714b0f2599ed48
parent 33670 02b7738aef6a
child 33672 8bde36ec8eb1
modernized structure Local_Theory;
src/FOL/ex/LocaleTest.thy
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOLCF/Tools/fixrec.ML
src/HOLCF/Tools/pcpodef.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/Isar/toplevel.ML
src/Pure/simplifier.ML
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4  begin
     1.5  
     1.6  thm lor_def
     1.7 -(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *)
     1.8 +(* Can we get rid the the additional hypothesis, caused by Local_Theory.notes? *)
     1.9  
    1.10  lemma "x || y = --(-- x && --y)"
    1.11    by (unfold lor_def) (rule refl)
     2.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 13 20:41:29 2009 +0100
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 13 21:11:15 2009 +0100
     2.3 @@ -38,7 +38,7 @@
     2.4    | SOME vc =>
     2.5        let
     2.6          fun store thm = Boogie_VCs.discharge (name, thm)
     2.7 -        fun after_qed [[thm]] = LocalTheory.theory (store thm)
     2.8 +        fun after_qed [[thm]] = Local_Theory.theory (store thm)
     2.9            | after_qed _ = I
    2.10        in
    2.11          lthy
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 20:41:29 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 21:11:15 2009 +0100
     3.3 @@ -561,19 +561,19 @@
     3.4              (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
     3.5            else (strong_raw_induct RSN (2, rev_mp),
     3.6              [ind_case_names, Rule_Cases.consumes 1]);
     3.7 -        val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note
     3.8 +        val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
     3.9            ((rec_qualified (Binding.name "strong_induct"),
    3.10              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
    3.11          val strong_inducts =
    3.12            Project_Rule.projects ctxt (1 upto length names) strong_induct';
    3.13        in
    3.14          ctxt' |>
    3.15 -        LocalTheory.note
    3.16 +        Local_Theory.note
    3.17            ((rec_qualified (Binding.name "strong_inducts"),
    3.18              [Attrib.internal (K ind_case_names),
    3.19               Attrib.internal (K (Rule_Cases.consumes 1))]),
    3.20             strong_inducts) |> snd |>
    3.21 -        LocalTheory.notes (map (fn ((name, elim), (_, cases)) =>
    3.22 +        Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
    3.23              ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    3.24                [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
    3.25                 Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
    3.26 @@ -663,7 +663,7 @@
    3.27        end) atoms
    3.28    in
    3.29      ctxt |>
    3.30 -    LocalTheory.notes (map (fn (name, ths) =>
    3.31 +    Local_Theory.notes (map (fn (name, ths) =>
    3.32          ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
    3.33            [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
    3.34        (names ~~ transp thss)) |> snd
     4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 20:41:29 2009 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 21:11:15 2009 +0100
     4.3 @@ -466,14 +466,14 @@
     4.4              NONE => (rec_qualified (Binding.name "strong_induct"),
     4.5                       rec_qualified (Binding.name "strong_inducts"))
     4.6            | SOME s => (Binding.name s, Binding.name (s ^ "s"));
     4.7 -        val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note
     4.8 +        val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note
     4.9            ((induct_name,
    4.10              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
    4.11          val strong_inducts =
    4.12            Project_Rule.projects ctxt' (1 upto length names) strong_induct'
    4.13        in
    4.14          ctxt' |>
    4.15 -        LocalTheory.note
    4.16 +        Local_Theory.note
    4.17            ((inducts_name,
    4.18              [Attrib.internal (K ind_case_names),
    4.19               Attrib.internal (K (Rule_Cases.consumes 1))]),
     5.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 20:41:29 2009 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 21:11:15 2009 +0100
     5.3 @@ -280,9 +280,8 @@
     5.4        else primrec_err ("functions " ^ commas_quote names2 ^
     5.5          "\nare not mutually recursive");
     5.6      val (defs_thms, lthy') = lthy |>
     5.7 -      set_group ? LocalTheory.set_group (serial ()) |>
     5.8 -      fold_map (apfst (snd o snd) oo
     5.9 -        LocalTheory.define Thm.definitionK o fst) defs';
    5.10 +      set_group ? Local_Theory.set_group (serial ()) |>
    5.11 +      fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
    5.12      val qualify = Binding.qualify false
    5.13        (space_implode "_" (map (Long_Name.base_name o #1) defs));
    5.14      val names_atts' = map (apfst qualify) names_atts;
    5.15 @@ -367,10 +366,11 @@
    5.16        (fn thss => fn goal_ctxt =>
    5.17           let
    5.18             val simps = ProofContext.export goal_ctxt lthy' (flat thss);
    5.19 -           val (simps', lthy'') = fold_map LocalTheory.note (names_atts' ~~ map single simps) lthy';
    5.20 +           val (simps', lthy'') =
    5.21 +            fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy';
    5.22           in
    5.23             lthy''
    5.24 -           |> LocalTheory.note ((qualify (Binding.name "simps"),
    5.25 +           |> Local_Theory.note ((qualify (Binding.name "simps"),
    5.26                  map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
    5.27                  maps snd simps')
    5.28             |> snd
     6.1 --- a/src/HOL/Statespace/state_space.ML	Fri Nov 13 20:41:29 2009 +0100
     6.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Nov 13 21:11:15 2009 +0100
     6.3 @@ -155,13 +155,13 @@
     6.4    thy 
     6.5    |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
     6.6    |> snd
     6.7 -  |> LocalTheory.exit;
     6.8 +  |> Local_Theory.exit;
     6.9  
    6.10  fun add_locale_cmd name expr elems thy =
    6.11    thy 
    6.12    |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
    6.13    |> snd
    6.14 -  |> LocalTheory.exit;
    6.15 +  |> Local_Theory.exit;
    6.16  
    6.17  type statespace_info =
    6.18   {args: (string * sort) list, (* type arguments *)
    6.19 @@ -350,8 +350,8 @@
    6.20  fun add_declaration name decl thy =
    6.21    thy
    6.22    |> Theory_Target.init name
    6.23 -  |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
    6.24 -  |> LocalTheory.exit_global;
    6.25 +  |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
    6.26 +  |> Local_Theory.exit_global;
    6.27  
    6.28  fun parent_components thy (Ts, pname, renaming) =
    6.29    let
    6.30 @@ -430,7 +430,7 @@
    6.31            let
    6.32              fun upd (n,v) =
    6.33                let
    6.34 -                val nT = ProofContext.infer_type (LocalTheory.target_of lthy) n
    6.35 +                val nT = ProofContext.infer_type (Local_Theory.target_of lthy) n
    6.36                in Context.proof_map
    6.37                    (update_declinfo (Morphism.term phi (Free (n,nT)),v))
    6.38                end;
     7.1 --- a/src/HOL/Tools/Function/fun.ML	Fri Nov 13 20:41:29 2009 +0100
     7.2 +++ b/src/HOL/Tools/Function/fun.ML	Fri Nov 13 21:11:15 2009 +0100
     7.3 @@ -153,11 +153,11 @@
     7.4  fun gen_fun add config fixes statements int lthy =
     7.5    let val group = serial () in
     7.6      lthy
     7.7 -      |> LocalTheory.set_group group
     7.8 +      |> Local_Theory.set_group group
     7.9        |> add fixes statements config
    7.10        |> by_pat_completeness_auto int
    7.11 -      |> LocalTheory.restore
    7.12 -      |> LocalTheory.set_group group
    7.13 +      |> Local_Theory.restore
    7.14 +      |> Local_Theory.set_group group
    7.15        |> termination_by (Function_Common.get_termination_prover lthy) int
    7.16    end;
    7.17  
     8.1 --- a/src/HOL/Tools/Function/function.ML	Fri Nov 13 20:41:29 2009 +0100
     8.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Nov 13 21:11:15 2009 +0100
     8.3 @@ -52,13 +52,14 @@
     8.4                     |> map (apfst (apfst extra_qualify))
     8.5  
     8.6        val (saved_spec_simps, lthy) =
     8.7 -        fold_map LocalTheory.note spec lthy
     8.8 +        fold_map Local_Theory.note spec lthy
     8.9  
    8.10        val saved_simps = maps snd saved_spec_simps
    8.11        val simps_by_f = sort saved_simps
    8.12  
    8.13        fun add_for_f fname simps =
    8.14 -        LocalTheory.note ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
    8.15 +        Local_Theory.note
    8.16 +          ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
    8.17          #> snd
    8.18      in
    8.19        (saved_simps,
    8.20 @@ -97,14 +98,14 @@
    8.21              |> addsmps (conceal_partial o Binding.qualify false "partial")
    8.22                   "psimps" conceal_partial psimp_attribs psimps
    8.23              ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
    8.24 -            ||>> LocalTheory.note ((conceal_partial (qualify "pinduct"),
    8.25 +            ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
    8.26                     [Attrib.internal (K (Rule_Cases.case_names cnames)),
    8.27                      Attrib.internal (K (Rule_Cases.consumes 1)),
    8.28                      Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
    8.29 -            ||>> LocalTheory.note ((Binding.conceal (qualify "termination"), []), [termination])
    8.30 -            ||> (snd o LocalTheory.note ((qualify "cases",
    8.31 +            ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
    8.32 +            ||> (snd o Local_Theory.note ((qualify "cases",
    8.33                     [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
    8.34 -            ||> fold_option (snd oo curry LocalTheory.note (qualify "domintros", [])) domintros
    8.35 +            ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
    8.36  
    8.37            val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
    8.38                                        pinducts=snd pinducts', termination=termination',
    8.39 @@ -114,11 +115,11 @@
    8.40              else Specification.print_consts lthy (K false) (map fst fixes)
    8.41          in
    8.42            lthy
    8.43 -          |> LocalTheory.declaration false (add_function_data o morph_function_data cdata)
    8.44 +          |> Local_Theory.declaration false (add_function_data o morph_function_data cdata)
    8.45          end
    8.46      in
    8.47        lthy
    8.48 -        |> is_external ? LocalTheory.set_group (serial ())
    8.49 +        |> is_external ? Local_Theory.set_group (serial ())
    8.50          |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    8.51          |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
    8.52      end
    8.53 @@ -152,7 +153,7 @@
    8.54            in
    8.55              lthy
    8.56              |> add_simps I "simps" I simp_attribs tsimps |> snd
    8.57 -            |> LocalTheory.note
    8.58 +            |> Local_Theory.note
    8.59                 ((qualify "induct",
    8.60                   [Attrib.internal (K (Rule_Cases.case_names case_names))]),
    8.61                  tinduct) |> snd
    8.62 @@ -174,12 +175,12 @@
    8.63  
    8.64  fun termination term_opt lthy =
    8.65    lthy
    8.66 -  |> LocalTheory.set_group (serial ())
    8.67 +  |> Local_Theory.set_group (serial ())
    8.68    |> termination_proof term_opt;
    8.69  
    8.70  fun termination_cmd term_opt lthy =
    8.71    lthy
    8.72 -  |> LocalTheory.set_group (serial ())
    8.73 +  |> Local_Theory.set_group (serial ())
    8.74    |> termination_proof_cmd term_opt;
    8.75  
    8.76  
     9.1 --- a/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 20:41:29 2009 +0100
     9.2 +++ b/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 21:11:15 2009 +0100
     9.3 @@ -456,7 +456,7 @@
     9.4    let
     9.5      val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
     9.6        lthy
     9.7 -      |> LocalTheory.conceal
     9.8 +      |> Local_Theory.conceal
     9.9        |> Inductive.add_inductive_i
    9.10            {quiet_mode = true,
    9.11              verbose = ! trace,
    9.12 @@ -470,7 +470,7 @@
    9.13            [] (* no parameters *)
    9.14            (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
    9.15            [] (* no special monos *)
    9.16 -      ||> LocalTheory.restore_naming lthy
    9.17 +      ||> Local_Theory.restore_naming lthy
    9.18  
    9.19      val cert = cterm_of (ProofContext.theory_of lthy)
    9.20      fun requantify orig_intro thm =
    9.21 @@ -518,7 +518,7 @@
    9.22          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
    9.23        |> Syntax.check_term lthy
    9.24    in
    9.25 -    LocalTheory.define ""
    9.26 +    Local_Theory.define ""
    9.27        ((Binding.name (function_name fname), mixfix),
    9.28          ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
    9.29    end
    9.30 @@ -928,7 +928,7 @@
    9.31            PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
    9.32  
    9.33        val (_, lthy) =
    9.34 -          LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
    9.35 +          Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
    9.36  
    9.37        val newthy = ProofContext.theory_of lthy
    9.38        val clauses = map (transfer_clause_ctx newthy) clauses
    10.1 --- a/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 20:41:29 2009 +0100
    10.2 +++ b/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 21:11:15 2009 +0100
    10.3 @@ -146,7 +146,7 @@
    10.4        fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
    10.5            let
    10.6              val ((f, (_, f_defthm)), lthy') =
    10.7 -              LocalTheory.define ""
    10.8 +              Local_Theory.define ""
    10.9                  ((Binding.name fname, mixfix),
   10.10                    ((Binding.conceal (Binding.name (fname ^ "_def")), []),
   10.11                    Term.subst_bound (fsum, f_def))) lthy
    11.1 --- a/src/HOL/Tools/Function/size.ML	Fri Nov 13 20:41:29 2009 +0100
    11.2 +++ b/src/HOL/Tools/Function/size.ML	Fri Nov 13 21:11:15 2009 +0100
    11.3 @@ -130,7 +130,7 @@
    11.4      fun define_overloaded (def_name, eq) lthy =
    11.5        let
    11.6          val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
    11.7 -        val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
    11.8 +        val ((_, (_, thm)), lthy') = lthy |> Local_Theory.define Thm.definitionK
    11.9            ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
   11.10          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
   11.11          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   11.12 @@ -149,7 +149,7 @@
   11.13        ||>> fold_map define_overloaded
   11.14          (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
   11.15        ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   11.16 -      ||> LocalTheory.exit_global;
   11.17 +      ||> Local_Theory.exit_global;
   11.18  
   11.19      val ctxt = ProofContext.init thy';
   11.20  
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 13 20:41:29 2009 +0100
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 13 21:11:15 2009 +0100
    12.3 @@ -137,8 +137,8 @@
    12.4    in
    12.5      if (is_inductify options) then
    12.6        let
    12.7 -        val lthy' = LocalTheory.theory (preprocess options const) lthy
    12.8 -          |> LocalTheory.checkpoint
    12.9 +        val lthy' = Local_Theory.theory (preprocess options const) lthy
   12.10 +          |> Local_Theory.checkpoint
   12.11          val const =
   12.12            case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
   12.13              SOME c => c
    13.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 13 20:41:29 2009 +0100
    13.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 13 21:11:15 2009 +0100
    13.3 @@ -2411,9 +2411,9 @@
    13.4    let
    13.5      val thy = ProofContext.theory_of lthy
    13.6      val const = prep_const thy raw_const
    13.7 -    val lthy' = LocalTheory.theory (PredData.map
    13.8 +    val lthy' = Local_Theory.theory (PredData.map
    13.9          (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
   13.10 -      |> LocalTheory.checkpoint
   13.11 +      |> Local_Theory.checkpoint
   13.12      val thy' = ProofContext.theory_of lthy'
   13.13      val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
   13.14      fun mk_cases const =
   13.15 @@ -2437,7 +2437,7 @@
   13.16          val global_thms = ProofContext.export goal_ctxt
   13.17            (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
   13.18        in
   13.19 -        goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
   13.20 +        goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
   13.21            (if is_random options then
   13.22              (add_equations options [const] #>
   13.23              add_quickcheck_equations options [const])
    14.1 --- a/src/HOL/Tools/inductive.ML	Fri Nov 13 20:41:29 2009 +0100
    14.2 +++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 21:11:15 2009 +0100
    14.3 @@ -469,7 +469,7 @@
    14.4      val facts = args |> map (fn ((a, atts), props) =>
    14.5        ((a, map (prep_att thy) atts),
    14.6          map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
    14.7 -  in lthy |> LocalTheory.notes facts |>> map snd end;
    14.8 +  in lthy |> Local_Theory.notes facts |>> map snd end;
    14.9  
   14.10  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
   14.11  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
   14.12 @@ -665,13 +665,13 @@
   14.13        else alt_name;
   14.14  
   14.15      val ((rec_const, (_, fp_def)), lthy') = lthy
   14.16 -      |> LocalTheory.conceal
   14.17 -      |> LocalTheory.define ""
   14.18 +      |> Local_Theory.conceal
   14.19 +      |> Local_Theory.define ""
   14.20          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
   14.21           ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
   14.22           fold_rev lambda params
   14.23             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   14.24 -      ||> LocalTheory.restore_naming lthy;
   14.25 +      ||> Local_Theory.restore_naming lthy;
   14.26      val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
   14.27        (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params)));
   14.28      val specs =
   14.29 @@ -688,14 +688,14 @@
   14.30                  make_args argTs (xs ~~ Ts)))))
   14.31            end) (cnames_syn ~~ cs);
   14.32      val (consts_defs, lthy'') = lthy'
   14.33 -      |> LocalTheory.conceal
   14.34 -      |> fold_map (LocalTheory.define "") specs
   14.35 -      ||> LocalTheory.restore_naming lthy';
   14.36 +      |> Local_Theory.conceal
   14.37 +      |> fold_map (Local_Theory.define "") specs
   14.38 +      ||> Local_Theory.restore_naming lthy';
   14.39      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
   14.40  
   14.41      val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
   14.42      val ((_, [mono']), lthy''') =
   14.43 -      LocalTheory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
   14.44 +      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
   14.45  
   14.46    in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
   14.47      list_comb (rec_const, params), preds, argTs, bs, xs)
   14.48 @@ -719,7 +719,7 @@
   14.49  
   14.50      val (intrs', lthy1) =
   14.51        lthy |>
   14.52 -      LocalTheory.notes
   14.53 +      Local_Theory.notes
   14.54          (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
   14.55            map (fn th => [([th],
   14.56             [Attrib.internal (K (Context_Rules.intro_query NONE)),
   14.57 @@ -727,16 +727,16 @@
   14.58        map (hd o snd);
   14.59      val (((_, elims'), (_, [induct'])), lthy2) =
   14.60        lthy1 |>
   14.61 -      LocalTheory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
   14.62 +      Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
   14.63        fold_map (fn (name, (elim, cases)) =>
   14.64 -        LocalTheory.note
   14.65 +        Local_Theory.note
   14.66            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
   14.67              [Attrib.internal (K (Rule_Cases.case_names cases)),
   14.68               Attrib.internal (K (Rule_Cases.consumes 1)),
   14.69               Attrib.internal (K (Induct.cases_pred name)),
   14.70               Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
   14.71          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
   14.72 -      LocalTheory.note
   14.73 +      Local_Theory.note
   14.74          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
   14.75            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
   14.76  
   14.77 @@ -745,7 +745,7 @@
   14.78        else
   14.79          let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
   14.80            lthy2 |>
   14.81 -          LocalTheory.notes [((rec_qualified true (Binding.name "inducts"), []),
   14.82 +          Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
   14.83              inducts |> map (fn (name, th) => ([th],
   14.84                [Attrib.internal (K ind_case_names),
   14.85                 Attrib.internal (K (Rule_Cases.consumes 1)),
   14.86 @@ -771,7 +771,7 @@
   14.87      val _ = message (quiet_mode andalso not verbose)
   14.88        ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
   14.89  
   14.90 -    val cnames = map (LocalTheory.full_name lthy o #1) cnames_syn;  (* FIXME *)
   14.91 +    val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn;  (* FIXME *)
   14.92      val ((intr_names, intr_atts), intr_ts) =
   14.93        apfst split_list (split_list (map (check_rule lthy cs params) intros));
   14.94  
   14.95 @@ -810,7 +810,7 @@
   14.96         induct = induct};
   14.97  
   14.98      val lthy3 = lthy2
   14.99 -      |> LocalTheory.declaration false (fn phi =>
  14.100 +      |> Local_Theory.declaration false (fn phi =>
  14.101          let val result' = morph_result phi result;
  14.102          in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
  14.103    in (result, lthy3) end;
  14.104 @@ -872,7 +872,7 @@
  14.105    in
  14.106      lthy
  14.107      |> mk_def flags cs intros monos ps preds
  14.108 -    ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs
  14.109 +    ||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
  14.110    end;
  14.111  
  14.112  fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
  14.113 @@ -886,7 +886,7 @@
  14.114        coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
  14.115    in
  14.116      lthy
  14.117 -    |> LocalTheory.set_group (serial ())
  14.118 +    |> Local_Theory.set_group (serial ())
  14.119      |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
  14.120    end;
  14.121  
  14.122 @@ -898,9 +898,9 @@
  14.123      val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
  14.124      val ctxt' = thy
  14.125        |> Theory_Target.init NONE
  14.126 -      |> LocalTheory.set_group group
  14.127 +      |> Local_Theory.set_group group
  14.128        |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
  14.129 -      |> LocalTheory.exit;
  14.130 +      |> Local_Theory.exit;
  14.131      val info = #2 (the_inductive ctxt' name);
  14.132    in (info, ProofContext.theory_of ctxt') end;
  14.133  
    15.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 20:41:29 2009 +0100
    15.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 21:11:15 2009 +0100
    15.3 @@ -14,7 +14,7 @@
    15.4  structure InductiveRealizer : INDUCTIVE_REALIZER =
    15.5  struct
    15.6  
    15.7 -(* FIXME: LocalTheory.note should return theorems with proper names! *)  (* FIXME ?? *)
    15.8 +(* FIXME: Local_Theory.note should return theorems with proper names! *)  (* FIXME ?? *)
    15.9  fun name_of_thm thm =
   15.10    (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
   15.11        [Thm.proof_of thm] [] of
    16.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 20:41:29 2009 +0100
    16.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 21:11:15 2009 +0100
    16.3 @@ -484,13 +484,13 @@
    16.4  
    16.5      (* define inductive sets using previously defined predicates *)
    16.6      val (defs, lthy2) = lthy1
    16.7 -      |> LocalTheory.conceal  (* FIXME ?? *)
    16.8 -      |> fold_map (LocalTheory.define "")
    16.9 +      |> Local_Theory.conceal  (* FIXME ?? *)
   16.10 +      |> fold_map (Local_Theory.define "")
   16.11          (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
   16.12             fold_rev lambda params (HOLogic.Collect_const U $
   16.13               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
   16.14             (cnames_syn ~~ cs_info ~~ preds))
   16.15 -      ||> LocalTheory.restore_naming lthy1;
   16.16 +      ||> Local_Theory.restore_naming lthy1;
   16.17  
   16.18      (* prove theorems for converting predicate to set notation *)
   16.19      val lthy3 = fold
   16.20 @@ -505,7 +505,7 @@
   16.21              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   16.22                [def, mem_Collect_eq, split_conv]) 1))
   16.23          in
   16.24 -          lthy |> LocalTheory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
   16.25 +          lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
   16.26              [Attrib.internal (K pred_set_conv_att)]),
   16.27                [conv_thm]) |> snd
   16.28          end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
   16.29 @@ -515,7 +515,7 @@
   16.30        if Binding.is_empty alt_name then
   16.31          Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
   16.32        else alt_name;
   16.33 -    val cnames = map (LocalTheory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
   16.34 +    val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
   16.35      val (intr_names, intr_atts) = split_list (map fst intros);
   16.36      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
   16.37      val (intrs', elims', induct, lthy4) =
    17.1 --- a/src/HOL/Tools/primrec.ML	Fri Nov 13 20:41:29 2009 +0100
    17.2 +++ b/src/HOL/Tools/primrec.ML	Fri Nov 13 21:11:15 2009 +0100
    17.3 @@ -259,7 +259,7 @@
    17.4      val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
    17.5    in
    17.6      lthy
    17.7 -    |> fold_map (LocalTheory.define Thm.definitionK) defs
    17.8 +    |> fold_map (Local_Theory.define Thm.definitionK) defs
    17.9      |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
   17.10    end;
   17.11  
   17.12 @@ -275,10 +275,10 @@
   17.13          map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
   17.14    in
   17.15      lthy
   17.16 -    |> set_group ? LocalTheory.set_group (serial ())
   17.17 +    |> set_group ? Local_Theory.set_group (serial ())
   17.18      |> add_primrec_simple fixes (map snd spec)
   17.19 -    |-> (fn (prefix, simps) => fold_map LocalTheory.note (attr_bindings prefix ~~ simps)
   17.20 -      #-> (fn simps' => LocalTheory.note (simp_attr_binding prefix, maps snd simps')))
   17.21 +    |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
   17.22 +      #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')))
   17.23      |>> snd
   17.24    end;
   17.25  
   17.26 @@ -294,14 +294,14 @@
   17.27      val lthy = Theory_Target.init NONE thy;
   17.28      val (simps, lthy') = add_primrec fixes specs lthy;
   17.29      val simps' = ProofContext.export lthy' lthy simps;
   17.30 -  in (simps', LocalTheory.exit_global lthy') end;
   17.31 +  in (simps', Local_Theory.exit_global lthy') end;
   17.32  
   17.33  fun add_primrec_overloaded ops fixes specs thy =
   17.34    let
   17.35      val lthy = Theory_Target.overloading ops thy;
   17.36      val (simps, lthy') = add_primrec fixes specs lthy;
   17.37      val simps' = ProofContext.export lthy' lthy simps;
   17.38 -  in (simps', LocalTheory.exit_global lthy') end;
   17.39 +  in (simps', Local_Theory.exit_global lthy') end;
   17.40  
   17.41  
   17.42  (* outer syntax *)
    18.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 20:41:29 2009 +0100
    18.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 21:11:15 2009 +0100
    18.3 @@ -190,7 +190,7 @@
    18.4        in
    18.5          lthy
    18.6          |> random_aux_primrec aux_eq'
    18.7 -        ||>> fold_map (LocalTheory.define Thm.definitionK) proj_defs
    18.8 +        ||>> fold_map (Local_Theory.define Thm.definitionK) proj_defs
    18.9          |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
   18.10        end;
   18.11  
   18.12 @@ -214,7 +214,7 @@
   18.13      lthy
   18.14      |> random_aux_primrec_multi (name ^ prfx) proto_eqs
   18.15      |-> (fn proto_simps => prove_simps proto_simps)
   18.16 -    |-> (fn simps => LocalTheory.note
   18.17 +    |-> (fn simps => Local_Theory.note
   18.18        ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
   18.19            [Simplifier.simp_add, Nitpick_Simps.add]), simps))
   18.20      |> snd
    19.1 --- a/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 20:41:29 2009 +0100
    19.2 +++ b/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 21:11:15 2009 +0100
    19.3 @@ -209,7 +209,7 @@
    19.4        | defs (l::[]) r = [one_def l r]
    19.5        | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
    19.6      val fixdefs = defs lhss fixpoint;
    19.7 -    val define_all = fold_map (LocalTheory.define Thm.definitionK);
    19.8 +    val define_all = fold_map (Local_Theory.define Thm.definitionK);
    19.9      val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
   19.10        |> define_all (map (apfst fst) fixes ~~ fixdefs);
   19.11      fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
   19.12 @@ -242,7 +242,7 @@
   19.13          ((thm_name, [src]), [thm])
   19.14        end;
   19.15      val (thmss, lthy'') = lthy'
   19.16 -      |> fold_map LocalTheory.note (induct_note :: map unfold_note unfold_thms);
   19.17 +      |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms);
   19.18    in
   19.19      (lthy'', names, fixdef_thms, map snd unfold_thms)
   19.20    end;
   19.21 @@ -464,7 +464,7 @@
   19.22        val simps2 : (Attrib.binding * thm list) list =
   19.23          map (apsnd (fn thm => [thm])) (flat simps);
   19.24        val (_, lthy'') = lthy'
   19.25 -        |> fold_map LocalTheory.note (simps1 @ simps2);
   19.26 +        |> fold_map Local_Theory.note (simps1 @ simps2);
   19.27      in
   19.28        lthy''
   19.29      end
    20.1 --- a/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 20:41:29 2009 +0100
    20.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 21:11:15 2009 +0100
    20.3 @@ -201,7 +201,7 @@
    20.4      val thy5 = lthy4
    20.5        |> Class.prove_instantiation_instance
    20.6            (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
    20.7 -      |> LocalTheory.exit_global;
    20.8 +      |> Local_Theory.exit_global;
    20.9    in ((info, below_definition), thy5) end;
   20.10  
   20.11  fun prepare_cpodef
    21.1 --- a/src/Pure/Isar/class.ML	Fri Nov 13 20:41:29 2009 +0100
    21.2 +++ b/src/Pure/Isar/class.ML	Fri Nov 13 21:11:15 2009 +0100
    21.3 @@ -281,7 +281,7 @@
    21.4    in
    21.5      thy
    21.6      |> Expression.add_locale bname Binding.empty supexpr elems
    21.7 -    |> snd |> LocalTheory.exit_global
    21.8 +    |> snd |> Local_Theory.exit_global
    21.9      |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
   21.10      ||> Theory.checkpoint
   21.11      |-> (fn (param_map, params, assm_axiom) =>
    22.1 --- a/src/Pure/Isar/class_target.ML	Fri Nov 13 20:41:29 2009 +0100
    22.2 +++ b/src/Pure/Isar/class_target.ML	Fri Nov 13 21:11:15 2009 +0100
    22.3 @@ -405,9 +405,9 @@
    22.4  
    22.5  fun mk_instantiation (arities, params) =
    22.6    Instantiation { arities = arities, params = params };
    22.7 -fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
    22.8 +fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy)
    22.9   of Instantiation data => data;
   22.10 -fun map_instantiation f = (LocalTheory.target o Instantiation.map)
   22.11 +fun map_instantiation f = (Local_Theory.target o Instantiation.map)
   22.12    (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
   22.13  
   22.14  fun the_instantiation lthy = case get_instantiation lthy
   22.15 @@ -526,14 +526,14 @@
   22.16  
   22.17  fun confirm_declaration b = (map_instantiation o apsnd)
   22.18    (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
   22.19 -  #> LocalTheory.target synchronize_inst_syntax
   22.20 +  #> Local_Theory.target synchronize_inst_syntax
   22.21  
   22.22  fun gen_instantiation_instance do_proof after_qed lthy =
   22.23    let
   22.24      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   22.25      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   22.26      fun after_qed' results =
   22.27 -      LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   22.28 +      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   22.29        #> after_qed;
   22.30    in
   22.31      lthy
   22.32 @@ -548,7 +548,7 @@
   22.33      (fn {context, ...} => tac context)) ts) lthy) I;
   22.34  
   22.35  fun prove_instantiation_exit tac = prove_instantiation_instance tac
   22.36 -  #> LocalTheory.exit_global;
   22.37 +  #> Local_Theory.exit_global;
   22.38  
   22.39  fun prove_instantiation_exit_result f tac x lthy =
   22.40    let
    23.1 --- a/src/Pure/Isar/expression.ML	Fri Nov 13 20:41:29 2009 +0100
    23.2 +++ b/src/Pure/Isar/expression.ML	Fri Nov 13 21:11:15 2009 +0100
    23.3 @@ -775,7 +775,7 @@
    23.4        |> Locale.register_locale binding (extraTs, params)
    23.5            (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
    23.6        |> Theory_Target.init (SOME name)
    23.7 -      |> fold (fn (kind, facts) => LocalTheory.notes_kind kind facts #> snd) notes';
    23.8 +      |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    23.9  
   23.10    in (name, loc_ctxt) end;
   23.11  
    24.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Nov 13 20:41:29 2009 +0100
    24.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Nov 13 21:11:15 2009 +0100
    24.3 @@ -181,7 +181,7 @@
    24.4  fun declaration pervasive (txt, pos) =
    24.5    txt |> ML_Context.expression pos
    24.6      "val declaration: Morphism.declaration"
    24.7 -    ("Context.map_proof (LocalTheory.declaration " ^ Bool.toString pervasive ^ " declaration)")
    24.8 +    ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
    24.9    |> Context.proof_map;
   24.10  
   24.11  
    25.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Nov 13 20:41:29 2009 +0100
    25.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 13 21:11:15 2009 +0100
    25.3 @@ -288,7 +288,7 @@
    25.4  (* use ML text *)
    25.5  
    25.6  fun propagate_env (context as Context.Proof lthy) =
    25.7 -      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
    25.8 +      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
    25.9    | propagate_env context = context;
   25.10  
   25.11  fun propagate_env_prf prf = Proof.map_contexts
    26.1 --- a/src/Pure/Isar/local_theory.ML	Fri Nov 13 20:41:29 2009 +0100
    26.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Nov 13 21:11:15 2009 +0100
    26.3 @@ -51,7 +51,7 @@
    26.4    val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
    26.5  end;
    26.6  
    26.7 -structure LocalTheory: LOCAL_THEORY =
    26.8 +structure Local_Theory: LOCAL_THEORY =
    26.9  struct
   26.10  
   26.11  (** local theory data **)
    27.1 --- a/src/Pure/Isar/overloading.ML	Fri Nov 13 20:41:29 2009 +0100
    27.2 +++ b/src/Pure/Isar/overloading.ML	Fri Nov 13 21:11:15 2009 +0100
    27.3 @@ -126,8 +126,8 @@
    27.4    fun init _ = [];
    27.5  );
    27.6  
    27.7 -val get_overloading = OverloadingData.get o LocalTheory.target_of;
    27.8 -val map_overloading = LocalTheory.target o OverloadingData.map;
    27.9 +val get_overloading = OverloadingData.get o Local_Theory.target_of;
   27.10 +val map_overloading = Local_Theory.target o OverloadingData.map;
   27.11  
   27.12  fun operation lthy b = get_overloading lthy
   27.13    |> get_first (fn ((c, _), (v, checked)) =>
   27.14 @@ -169,7 +169,7 @@
   27.15    (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
   27.16  
   27.17  fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
   27.18 -  #> LocalTheory.target synchronize_syntax
   27.19 +  #> Local_Theory.target synchronize_syntax
   27.20  
   27.21  fun conclude lthy =
   27.22    let
    28.1 --- a/src/Pure/Isar/spec_rules.ML	Fri Nov 13 20:41:29 2009 +0100
    28.2 +++ b/src/Pure/Isar/spec_rules.ML	Fri Nov 13 21:11:15 2009 +0100
    28.3 @@ -41,7 +41,7 @@
    28.4  val get = Item_Net.content o Rules.get o Context.Proof;
    28.5  val get_global = Item_Net.content o Rules.get o Context.Theory;
    28.6  
    28.7 -fun add class (ts, ths) = LocalTheory.declaration true
    28.8 +fun add class (ts, ths) = Local_Theory.declaration true
    28.9    (fn phi =>
   28.10      let
   28.11        val ts' = map (Morphism.term phi) ts;
    29.1 --- a/src/Pure/Isar/specification.ML	Fri Nov 13 20:41:29 2009 +0100
    29.2 +++ b/src/Pure/Isar/specification.ML	Fri Nov 13 21:11:15 2009 +0100
    29.3 @@ -202,18 +202,18 @@
    29.4            in (b, mx) end);
    29.5      val name = Thm.def_binding_optional b raw_name;
    29.6      val ((lhs, (_, raw_th)), lthy2) = lthy
    29.7 -      |> LocalTheory.define Thm.definitionK
    29.8 +      |> Local_Theory.define Thm.definitionK
    29.9          (var, ((Binding.suffix_name "_raw" name, []), rhs));
   29.10  
   29.11      val th = prove lthy2 raw_th;
   29.12      val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
   29.13  
   29.14      val ([(def_name, [th'])], lthy4) = lthy3
   29.15 -      |> LocalTheory.notes_kind Thm.definitionK
   29.16 +      |> Local_Theory.notes_kind Thm.definitionK
   29.17          [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
   29.18              Code.add_default_eqn_attrib :: atts), [([th], [])])];
   29.19  
   29.20 -    val lhs' = Morphism.term (LocalTheory.target_morphism lthy4) lhs;
   29.21 +    val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
   29.22      val _ =
   29.23        if not do_print then ()
   29.24        else print_consts lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   29.25 @@ -243,7 +243,7 @@
   29.26            in (b, mx) end);
   29.27      val lthy' = lthy
   29.28        |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
   29.29 -      |> LocalTheory.abbrev mode (var, rhs) |> snd
   29.30 +      |> Local_Theory.abbrev mode (var, rhs) |> snd
   29.31        |> ProofContext.restore_syntax_mode lthy;
   29.32  
   29.33      val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
   29.34 @@ -256,7 +256,7 @@
   29.35  (* notation *)
   29.36  
   29.37  fun gen_notation prep_const add mode args lthy =
   29.38 -  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
   29.39 +  lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
   29.40  
   29.41  val notation = gen_notation (K I);
   29.42  val notation_cmd = gen_notation ProofContext.read_const;
   29.43 @@ -270,7 +270,7 @@
   29.44      val facts = raw_facts |> map (fn ((name, atts), bs) =>
   29.45        ((name, map attrib atts),
   29.46          bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   29.47 -    val (res, lthy') = lthy |> LocalTheory.notes_kind kind facts;
   29.48 +    val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts;
   29.49      val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
   29.50    in (res, lthy') end;
   29.51  
   29.52 @@ -345,7 +345,7 @@
   29.53  fun gen_theorem prep_att prep_stmt
   29.54      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
   29.55    let
   29.56 -    val _ = LocalTheory.affirm lthy;
   29.57 +    val _ = Local_Theory.affirm lthy;
   29.58      val thy = ProofContext.theory_of lthy;
   29.59  
   29.60      val attrib = prep_att thy;
   29.61 @@ -359,7 +359,7 @@
   29.62          burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
   29.63        in
   29.64          lthy
   29.65 -        |> LocalTheory.notes_kind kind
   29.66 +        |> Local_Theory.notes_kind kind
   29.67            (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
   29.68          |> (fn (res, lthy') =>
   29.69            if Binding.is_empty name andalso null atts then
   29.70 @@ -367,7 +367,7 @@
   29.71            else
   29.72              let
   29.73                val ([(res_name, _)], lthy'') = lthy'
   29.74 -                |> LocalTheory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
   29.75 +                |> Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
   29.76                val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
   29.77              in lthy'' end)
   29.78          |> after_qed results'
    30.1 --- a/src/Pure/Isar/theory_target.ML	Fri Nov 13 20:41:29 2009 +0100
    30.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Nov 13 21:11:15 2009 +0100
    30.3 @@ -77,14 +77,14 @@
    30.4  
    30.5  fun direct_decl decl =
    30.6    let val decl0 = Morphism.form decl in
    30.7 -    LocalTheory.theory (Context.theory_map decl0) #>
    30.8 -    LocalTheory.target (Context.proof_map decl0)
    30.9 +    Local_Theory.theory (Context.theory_map decl0) #>
   30.10 +    Local_Theory.target (Context.proof_map decl0)
   30.11    end;
   30.12  
   30.13  fun target_decl add (Target {target, ...}) pervasive decl lthy =
   30.14    let
   30.15 -    val global_decl = Morphism.transform (LocalTheory.global_morphism lthy) decl;
   30.16 -    val target_decl = Morphism.transform (LocalTheory.target_morphism lthy) decl;
   30.17 +    val global_decl = Morphism.transform (Local_Theory.global_morphism lthy) decl;
   30.18 +    val target_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
   30.19    in
   30.20      if target = "" then
   30.21        lthy
   30.22 @@ -92,7 +92,7 @@
   30.23      else
   30.24        lthy
   30.25        |> pervasive ? direct_decl global_decl
   30.26 -      |> LocalTheory.target (add target target_decl)
   30.27 +      |> Local_Theory.target (add target target_decl)
   30.28    end;
   30.29  
   30.30  in
   30.31 @@ -104,8 +104,8 @@
   30.32  end;
   30.33  
   30.34  fun class_target (Target {target, ...}) f =
   30.35 -  LocalTheory.raw_theory f #>
   30.36 -  LocalTheory.target (Class_Target.refresh_syntax target);
   30.37 +  Local_Theory.raw_theory f #>
   30.38 +  Local_Theory.target (Class_Target.refresh_syntax target);
   30.39  
   30.40  
   30.41  (* notes *)
   30.42 @@ -161,19 +161,19 @@
   30.43      val thy = ProofContext.theory_of lthy;
   30.44      val facts' = facts
   30.45        |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
   30.46 -          (LocalTheory.full_name lthy (fst a))) bs))
   30.47 +          (Local_Theory.full_name lthy (fst a))) bs))
   30.48        |> PureThy.map_facts (import_export_proof lthy);
   30.49      val local_facts = PureThy.map_facts #1 facts'
   30.50        |> Attrib.map_facts (Attrib.attribute_i thy);
   30.51      val target_facts = PureThy.map_facts #1 facts'
   30.52 -      |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy));
   30.53 +      |> is_locale ? Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy));
   30.54      val global_facts = PureThy.map_facts #2 facts'
   30.55        |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
   30.56    in
   30.57      lthy
   30.58 -    |> LocalTheory.theory (PureThy.note_thmss kind global_facts #> snd)
   30.59 -    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
   30.60 -    |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
   30.61 +    |> Local_Theory.theory (PureThy.note_thmss kind global_facts #> snd)
   30.62 +    |> not is_locale ? Local_Theory.target (ProofContext.note_thmss kind global_facts #> snd)
   30.63 +    |> is_locale ? Local_Theory.target (Locale.add_thmss target kind target_facts)
   30.64      |> ProofContext.note_thmss kind local_facts
   30.65    end;
   30.66  
   30.67 @@ -212,22 +212,22 @@
   30.68  
   30.69  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   30.70    let
   30.71 -    val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   30.72 +    val xs = filter depends (#1 (ProofContext.inferred_fixes (Local_Theory.target_of lthy)));
   30.73      val U = map #2 xs ---> T;
   30.74      val (mx1, mx2, mx3) = fork_mixfix ta mx;
   30.75      val (const, lthy') = lthy |>
   30.76        (case Class_Target.instantiation_param lthy b of
   30.77          SOME c' =>
   30.78            if mx3 <> NoSyn then syntax_error c'
   30.79 -          else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
   30.80 +          else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
   30.81              ##> Class_Target.confirm_declaration b
   30.82          | NONE =>
   30.83              (case Overloading.operation lthy b of
   30.84                SOME (c', _) =>
   30.85                  if mx3 <> NoSyn then syntax_error c'
   30.86 -                else LocalTheory.theory_result (Overloading.declare (c', U))
   30.87 +                else Local_Theory.theory_result (Overloading.declare (c', U))
   30.88                    ##> Overloading.confirm b
   30.89 -            | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
   30.90 +            | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
   30.91      val t = Term.list_comb (const, map Free xs);
   30.92    in
   30.93      lthy'
   30.94 @@ -242,7 +242,7 @@
   30.95  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   30.96    let
   30.97      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   30.98 -    val target_ctxt = LocalTheory.target_of lthy;
   30.99 +    val target_ctxt = Local_Theory.target_of lthy;
  30.100  
  30.101      val (mx1, mx2, mx3) = fork_mixfix ta mx;
  30.102      val t' = Assumption.export_term lthy target_ctxt t;
  30.103 @@ -253,14 +253,14 @@
  30.104    in
  30.105      lthy |>
  30.106       (if is_locale then
  30.107 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
  30.108 +        Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
  30.109          #-> (fn (lhs, _) =>
  30.110            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
  30.111              term_syntax ta false (locale_const ta prmode ((b, mx2), lhs')) #>
  30.112              is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
  30.113            end)
  30.114        else
  30.115 -        LocalTheory.theory
  30.116 +        Local_Theory.theory
  30.117            (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
  30.118             Sign.notation true prmode [(lhs, mx3)])))
  30.119      |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
  30.120 @@ -278,7 +278,7 @@
  30.121      val name' = Thm.def_binding_optional b name;
  30.122      val (rhs', rhs_conv) =
  30.123        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
  30.124 -    val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
  30.125 +    val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
  30.126      val T = Term.fastype_of rhs;
  30.127  
  30.128      (*const*)
  30.129 @@ -287,7 +287,7 @@
  30.130  
  30.131      (*def*)
  30.132      val (global_def, lthy3) = lthy2
  30.133 -      |> LocalTheory.theory_result
  30.134 +      |> Local_Theory.theory_result
  30.135          (case Overloading.operation lthy b of
  30.136            SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
  30.137          | NONE =>
  30.138 @@ -324,7 +324,7 @@
  30.139  
  30.140  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
  30.141    Data.put ta #>
  30.142 -  LocalTheory.init (Long_Name.base_name target)
  30.143 +  Local_Theory.init (Long_Name.base_name target)
  30.144     {pretty = pretty ta,
  30.145      abbrev = abbrev ta,
  30.146      define = define ta,
  30.147 @@ -333,7 +333,7 @@
  30.148      term_syntax = term_syntax ta,
  30.149      declaration = declaration ta,
  30.150      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
  30.151 -    exit = LocalTheory.target_of o
  30.152 +    exit = Local_Theory.target_of o
  30.153        (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
  30.154         else if not (null overloading) then Overloading.conclude
  30.155         else I)}
    31.1 --- a/src/Pure/Isar/toplevel.ML	Fri Nov 13 20:41:29 2009 +0100
    31.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Nov 13 21:11:15 2009 +0100
    31.3 @@ -105,16 +105,16 @@
    31.4  type generic_theory = Context.generic;    (*theory or local_theory*)
    31.5  
    31.6  val loc_init = Theory_Target.context;
    31.7 -val loc_exit = LocalTheory.exit_global;
    31.8 +val loc_exit = Local_Theory.exit_global;
    31.9  
   31.10  fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   31.11    | loc_begin NONE (Context.Proof lthy) = lthy
   31.12    | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
   31.13  
   31.14  fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
   31.15 -  | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore
   31.16 +  | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
   31.17    | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
   31.18 -      Context.Proof (LocalTheory.reinit (LocalTheory.raw_theory (K (loc_exit lthy')) lthy));
   31.19 +      Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy));
   31.20  
   31.21  
   31.22  (* datatype node *)
   31.23 @@ -193,7 +193,7 @@
   31.24  
   31.25  (* print state *)
   31.26  
   31.27 -val pretty_context = LocalTheory.pretty o Context.cases (Theory_Target.init NONE) I;
   31.28 +val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
   31.29  
   31.30  fun print_state_context state =
   31.31    (case try node_of state of
   31.32 @@ -259,7 +259,7 @@
   31.33    | stale_error some = some;
   31.34  
   31.35  fun map_theory f (Theory (gthy, ctxt)) =
   31.36 -      Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, ctxt)
   31.37 +      Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt)
   31.38    | map_theory _ node = node;
   31.39  
   31.40  in
    32.1 --- a/src/Pure/simplifier.ML	Fri Nov 13 20:41:29 2009 +0100
    32.2 +++ b/src/Pure/simplifier.ML	Fri Nov 13 21:11:15 2009 +0100
    32.3 @@ -177,7 +177,7 @@
    32.4  fun gen_simproc prep {name, lhss, proc, identifier} lthy =
    32.5    let
    32.6      val b = Binding.name name;
    32.7 -    val naming = LocalTheory.naming_of lthy;
    32.8 +    val naming = Local_Theory.naming_of lthy;
    32.9      val simproc = make_simproc
   32.10        {name = Name_Space.full_name naming b,
   32.11         lhss =
   32.12 @@ -191,7 +191,7 @@
   32.13         proc = proc,
   32.14         identifier = identifier};
   32.15    in
   32.16 -    lthy |> LocalTheory.declaration false (fn phi =>
   32.17 +    lthy |> Local_Theory.declaration false (fn phi =>
   32.18        let
   32.19          val b' = Morphism.binding phi b;
   32.20          val simproc' = morph_simproc phi simproc;
   32.21 @@ -335,7 +335,8 @@
   32.22      "declaration of Simplifier rewrite rule" #>
   32.23    Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
   32.24      "declaration of Simplifier congruence rule" #>
   32.25 -  Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
   32.26 +  Attrib.setup (Binding.name "simproc") simproc_att
   32.27 +    "declaration of simplification procedures" #>
   32.28    Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
   32.29  
   32.30