--- 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)
--- 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
--- 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
--- 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))]),
--- 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
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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';
--- 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
--- 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])
--- 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;
--- 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
--- 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) =
--- 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 *)
--- 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
--- 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
--- 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
--- 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) =>
--- 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
--- 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;
--- 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;
--- 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
--- 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 **)
--- 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
--- 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;
--- 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'
--- 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)}
--- 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
--- 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"));