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