--- a/src/Pure/Isar/attrib.ML Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Apr 01 19:07:32 2012 +0200
@@ -25,6 +25,12 @@
val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
+ val global_notes: string -> (binding * (thm list * src list) list) list ->
+ theory -> (string * thm list) list * theory
+ val local_notes: string -> (binding * (thm list * src list) list) list ->
+ Proof.context -> (string * thm list) list * Proof.context
+ val generic_notes: string -> (binding * (thm list * src list) list) list ->
+ Context.generic -> (string * thm list) list * Context.generic
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -138,6 +144,15 @@
(* fact expressions *)
+fun global_notes kind facts thy = thy |>
+ Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
+
+fun local_notes kind facts ctxt = ctxt |>
+ Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
+
+fun generic_notes kind facts context = context |>
+ Context.mapping_result (global_notes kind facts) (local_notes kind facts);
+
fun eval_thms ctxt srcs = ctxt
|> Proof_Context.note_thmss ""
(map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
--- a/src/Pure/Isar/bundle.ML Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/bundle.ML Sun Apr 01 19:07:32 2012 +0200
@@ -87,11 +87,8 @@
local
fun gen_includes prep args ctxt =
- let
- val decls = maps (the_bundle ctxt o prep ctxt) args;
- val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
- val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
- in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
+ let val decls = maps (the_bundle ctxt o prep ctxt) args
+ in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
fun gen_context prep args (Context.Theory thy) =
Named_Target.theory_init thy
--- a/src/Pure/Isar/element.ML Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/element.ML Sun Apr 01 19:07:32 2012 +0200
@@ -51,8 +51,6 @@
val satisfy_morphism: witness list -> morphism
val eq_morphism: theory -> thm list -> morphism option
val transfer_morphism: theory -> morphism
- val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
- Context.generic -> (string * thm list) list * Context.generic
val init: context_i -> Context.generic -> Context.generic
val activate_i: context_i -> Proof.context -> context_i * Proof.context
val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -483,16 +481,6 @@
(* init *)
-fun generic_note_thmss kind facts context =
- let
- val facts' =
- Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts;
- in
- context |> Context.mapping_result
- (Global_Theory.note_thmss kind facts')
- (Proof_Context.note_thmss kind facts')
- end;
-
fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
| init (Constrains _) = I
| init (Assumes asms) = Context.map_proof (fn ctxt =>
@@ -514,7 +502,7 @@
|> fold Variable.auto_fixes (map #1 asms)
|> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
- | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
+ | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
(* activate *)
--- a/src/Pure/Isar/expression.ML Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/expression.ML Sun Apr 01 19:07:32 2012 +0200
@@ -816,7 +816,7 @@
local
fun note_eqns_register deps witss attrss eqns export export' =
- Element.generic_note_thmss Thm.lemmaK
+ Attrib.generic_notes Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
#-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
#-> (fn eqns => fold (fn ((dep, morph), wits) =>
@@ -885,12 +885,10 @@
fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
-
val facts =
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
val eqns' = ctxt
- |> Proof_Context.note_thmss Thm.lemmaK (Attrib.map_facts (map (Attrib.attribute_i thy)) facts)
+ |> Attrib.local_notes Thm.lemmaK facts
|-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
|> fst; (* FIXME duplication to add_thmss *)
in
--- a/src/Pure/Isar/generic_target.ML Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Apr 01 19:07:32 2012 +0200
@@ -142,7 +142,6 @@
fun notes target_notes kind facts lthy =
let
- val thy = Proof_Context.theory_of lthy;
val facts' = facts
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
(Local_Theory.full_name lthy (fst a))) bs))
@@ -152,7 +151,7 @@
in
lthy
|> target_notes kind global_facts local_facts
- |> Proof_Context.note_thmss kind (Attrib.map_facts (map (Attrib.attribute_i thy)) local_facts)
+ |> Attrib.local_notes kind local_facts
end;
@@ -215,15 +214,9 @@
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
in ((lhs, def), lthy3) end;
-fun theory_notes kind global_facts lthy =
- let
- val thy = Proof_Context.theory_of lthy;
- val global_facts' = Attrib.map_facts (map (Attrib.attribute_i thy)) global_facts;
- in
- lthy
- |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
- |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
- end;
+fun theory_notes kind global_facts =
+ Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
+ Local_Theory.target (Attrib.local_notes kind global_facts #> snd);
fun theory_abbrev prmode ((b, mx), t) =
Local_Theory.background_theory
--- a/src/Pure/Isar/locale.ML Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/locale.ML Sun Apr 01 19:07:32 2012 +0200
@@ -535,18 +535,13 @@
fun add_thmss _ _ [] ctxt = ctxt
| add_thmss loc kind facts ctxt =
ctxt
- |> Proof_Context.note_thmss kind
- (Attrib.map_facts (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) facts)
- |> snd
+ |> Attrib.local_notes kind facts |> snd
|> Proof_Context.background_theory
((change_locale loc o apfst o apsnd) (cons ((kind, facts), serial ())) #>
(* Registrations *)
- (fn thy => fold_rev (fn (_, morph) =>
- let
- val facts' = facts
- |> Element.transform_facts morph
- |> Attrib.map_facts (map (Attrib.attribute_i thy));
- in snd o Global_Theory.note_thmss kind facts' end)
+ (fn thy =>
+ fold_rev (fn (_, morph) =>
+ snd o Attrib.global_notes kind (Element.transform_facts morph facts))
(registrations_of (Context.Theory thy) loc) thy));
--- a/src/Tools/interpretation_with_defs.ML Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Tools/interpretation_with_defs.ML Sun Apr 01 19:07:32 2012 +0200
@@ -23,7 +23,7 @@
map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
maps snd;
in
- Element.generic_note_thmss Thm.lemmaK
+ Attrib.generic_notes Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
#-> (fn facts => `(fn context => meta_rewrite context facts))
#-> (fn eqns => fold (fn ((dep, morph), wits) =>