# HG changeset patch # User wenzelm # Date 1258143075 -3600 # Node ID 4b0f2599ed48bdac6bafb29be58cd68310cd7afb # Parent 02b7738aef6a341350bbae0fa35fe4921cf1bfb2 modernized structure Local_Theory; diff -r 02b7738aef6a -r 4b0f2599ed48 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Fri Nov 13 20:41:29 2009 +0100 +++ b/src/FOL/ex/LocaleTest.thy Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Nov 13 21:11:15 2009 +0100 @@ -561,19 +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') = 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]); val strong_inducts = 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], [])])) @@ -663,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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 13 21:11:15 2009 +0100 @@ -466,14 +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') = ctxt |> LocalTheory.note + val ((_, [strong_induct']), ctxt') = ctxt |> Local_Theory.note ((induct_name, 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 21:11:15 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,10 +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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/Function/fun.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/Function/function.ML Fri Nov 13 21:11:15 2009 +0100 @@ -52,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 = - LocalTheory.note ((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, @@ -97,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 - ||>> LocalTheory.note ((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) - ||>> LocalTheory.note ((Binding.conceal (qualify "termination"), []), [termination]) - ||> (snd o LocalTheory.note ((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 LocalTheory.note (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', @@ -114,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 @@ -152,7 +153,7 @@ in lthy |> add_simps I "simps" I simp_attribs tsimps |> snd - |> LocalTheory.note + |> Local_Theory.note ((qualify "induct", [Attrib.internal (K (Rule_Cases.case_names case_names))]), tinduct) |> snd @@ -174,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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Fri Nov 13 21:11:15 2009 +0100 @@ -456,7 +456,7 @@ 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, @@ -470,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 = @@ -518,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 @@ -928,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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/Function/size.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Nov 13 21:11:15 2009 +0100 @@ -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; @@ -665,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 = @@ -688,14 +688,14 @@ 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) @@ -719,7 +719,7 @@ val (intrs', lthy1) = lthy |> - LocalTheory.notes + Local_Theory.notes (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (Context_Rules.intro_query NONE)), @@ -727,16 +727,16 @@ map (hd o snd); val (((_, elims'), (_, [induct'])), lthy2) = lthy1 |> - LocalTheory.note ((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 + 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 + Local_Theory.note ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); @@ -745,7 +745,7 @@ else let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in lthy2 |> - LocalTheory.notes [((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)), @@ -771,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)); @@ -810,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; @@ -872,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 = @@ -886,7 +886,7 @@ 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; @@ -898,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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 21:11:15 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 diff -r 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/inductive_set.ML Fri Nov 13 21:11:15 2009 +0100 @@ -484,13 +484,13 @@ (* 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 ((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,7 +515,7 @@ 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) = diff -r 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/primrec.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOL/Tools/quickcheck_generators.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOLCF/Tools/fixrec.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/class.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/expression.ML Fri Nov 13 21:11:15 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 kind facts #> snd) notes'; + |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; diff -r 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/local_theory.ML Fri Nov 13 21:11:15 2009 +0100 @@ -51,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 **) diff -r 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/overloading.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/spec_rules.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/specification.ML Fri Nov 13 21:11:15 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.notes_kind Thm.definitionK + |> 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 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,7 +359,7 @@ burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results in lthy - |> LocalTheory.notes_kind kind + |> 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 @@ -367,7 +367,7 @@ else let val ([(res_name, _)], lthy'') = lthy' - |> LocalTheory.notes_kind 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 13 21:11:15 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 => @@ -324,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, @@ -333,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 02b7738aef6a -r 4b0f2599ed48 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Nov 13 21:11:15 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 02b7738aef6a -r 4b0f2599ed48 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/simplifier.ML Fri Nov 13 21:11:15 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"));