merged
authorwenzelm
Wed Aug 13 20:43:19 2014 +0200 (2014-08-13)
changeset 579303b4deb99a932
parent 57922 dc78785427d0
parent 57929 c5063c033a5a
child 57931 4e2cbff02f23
merged
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 13 17:17:51 2014 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 13 20:43:19 2014 +0200
     1.3 @@ -11,6 +11,10 @@
     1.4    val empty_binding: binding
     1.5    val is_empty_binding: binding -> bool
     1.6    val print_attributes: Proof.context -> unit
     1.7 +  val define_global: Binding.binding -> (Args.src -> attribute) ->
     1.8 +    string -> theory -> string * theory
     1.9 +  val define: Binding.binding -> (Args.src -> attribute) ->
    1.10 +    string -> local_theory -> string * local_theory
    1.11    val check_name_generic: Context.generic -> xstring * Position.T -> string
    1.12    val check_name: Proof.context -> xstring * Position.T -> string
    1.13    val check_src: Proof.context -> src -> src
    1.14 @@ -35,6 +39,8 @@
    1.15      Context.generic -> (string * thm list) list * Context.generic
    1.16    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    1.17    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    1.18 +  val local_setup: Binding.binding -> attribute context_parser -> string ->
    1.19 +    local_theory -> local_theory
    1.20    val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    1.21    val internal: (morphism -> attribute) -> src
    1.22    val add_del: attribute -> attribute -> attribute context_parser
    1.23 @@ -74,7 +80,6 @@
    1.24  (* source and bindings *)
    1.25  
    1.26  type src = Args.src;
    1.27 -
    1.28  type binding = binding * src list;
    1.29  
    1.30  val empty_binding: binding = (Binding.empty, []);
    1.31 @@ -86,7 +91,7 @@
    1.32  
    1.33  (* theory data *)
    1.34  
    1.35 -structure Attributes = Theory_Data
    1.36 +structure Attributes = Generic_Data
    1.37  (
    1.38    type T = ((src -> attribute) * string) Name_Space.table;
    1.39    val empty : T = Name_Space.empty_table "attribute";
    1.40 @@ -94,11 +99,17 @@
    1.41    fun merge data : T = Name_Space.merge_tables data;
    1.42  );
    1.43  
    1.44 -val get_attributes = Attributes.get o Context.theory_of;
    1.45 +val get_attributes = Attributes.get o Context.Proof;
    1.46 +
    1.47 +fun transfer_attributes thy ctxt =
    1.48 +  let
    1.49 +    val attribs' =
    1.50 +      Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt);
    1.51 +  in Context.proof_map (Attributes.put attribs') ctxt end;
    1.52  
    1.53  fun print_attributes ctxt =
    1.54    let
    1.55 -    val attribs = get_attributes (Context.Proof ctxt);
    1.56 +    val attribs = get_attributes ctxt;
    1.57      fun prt_attr (name, (_, "")) = Pretty.mark_str name
    1.58        | prt_attr (name, (_, comment)) =
    1.59            Pretty.block
    1.60 @@ -108,20 +119,46 @@
    1.61      |> Pretty.writeln_chunks
    1.62    end;
    1.63  
    1.64 -val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof;
    1.65 +val attribute_space = Name_Space.space_of_table o get_attributes;
    1.66 +
    1.67 +
    1.68 +(* define *)
    1.69 +
    1.70 +fun define_global binding att comment thy =
    1.71 +  let
    1.72 +    val context = Context.Theory thy;
    1.73 +    val (name, attribs') =
    1.74 +      Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
    1.75 +  in (name, Context.the_theory (Attributes.put attribs' context)) end;
    1.76  
    1.77 -fun add_attribute name att comment thy = thy
    1.78 -  |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
    1.79 +fun define binding att comment lthy =
    1.80 +  let
    1.81 +    val standard_morphism =
    1.82 +      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    1.83 +    val att0 = att o Args.transform_values standard_morphism;
    1.84 +  in
    1.85 +    lthy
    1.86 +    |> Local_Theory.background_theory_result (define_global binding att0 comment)
    1.87 +    |-> (fn name =>
    1.88 +      Local_Theory.map_contexts
    1.89 +        (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt)
    1.90 +      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    1.91 +          let
    1.92 +            val naming = Name_Space.naming_of context;
    1.93 +            val binding' = Morphism.binding phi binding;
    1.94 +          in Attributes.map (Name_Space.alias_table naming binding' name) context end)
    1.95 +      #> pair name)
    1.96 +  end;
    1.97  
    1.98  
    1.99  (* check *)
   1.100  
   1.101 -fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
   1.102 +fun check_name_generic context = #1 o Name_Space.check context (Attributes.get context);
   1.103  val check_name = check_name_generic o Context.Proof;
   1.104  
   1.105  fun check_src ctxt src =
   1.106   (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
   1.107 -  #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src));
   1.108 +  #1 (Args.check_src ctxt (get_attributes ctxt) src));
   1.109  
   1.110  
   1.111  (* pretty printing *)
   1.112 @@ -133,7 +170,7 @@
   1.113  (* get attributes *)
   1.114  
   1.115  fun attribute_generic context =
   1.116 -  let val table = get_attributes context
   1.117 +  let val table = Attributes.get context
   1.118    in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
   1.119  
   1.120  val attribute = attribute_generic o Context.Proof;
   1.121 @@ -171,10 +208,11 @@
   1.122  
   1.123  (* attribute setup *)
   1.124  
   1.125 -fun setup name scan =
   1.126 -  add_attribute name
   1.127 -    (fn src => fn (ctxt, th) =>
   1.128 -      let val (a, ctxt') = Args.syntax_generic scan src ctxt in a (ctxt', th) end);
   1.129 +fun attribute_syntax scan src (context, th) =
   1.130 +  let val (a, context') = Args.syntax_generic scan src context in a (context', th) end;
   1.131 +
   1.132 +fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
   1.133 +fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
   1.134  
   1.135  fun attribute_setup name source cmt =
   1.136    Context.theory_map (ML_Context.expression (#pos source)
     2.1 --- a/src/Pure/Isar/expression.ML	Wed Aug 13 17:17:51 2014 +0200
     2.2 +++ b/src/Pure/Isar/expression.ML	Wed Aug 13 20:43:19 2014 +0200
     2.3 @@ -924,7 +924,7 @@
     2.4  fun subscribe_or_activate lthy =
     2.5    if Named_Target.is_theory lthy
     2.6    then Local_Theory.subscription
     2.7 -  else Local_Theory.activate;
     2.8 +  else Locale.activate_fragment;
     2.9  
    2.10  fun subscribe_locale_only lthy =
    2.11    let
    2.12 @@ -964,7 +964,7 @@
    2.13      (K Local_Theory.subscription) expression raw_eqns;
    2.14  
    2.15  fun ephemeral_interpretation x =
    2.16 -  gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;
    2.17 +  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
    2.18  
    2.19  fun interpretation x =
    2.20    gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
     3.1 --- a/src/Pure/Isar/generic_target.ML	Wed Aug 13 17:17:51 2014 +0200
     3.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Aug 13 20:43:19 2014 +0200
     3.3 @@ -358,6 +358,6 @@
     3.4  
     3.5  fun locale_dependency locale dep_morph mixin export =
     3.6    (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
     3.7 -  #> Local_Theory.activate_nonbrittle dep_morph mixin export;
     3.8 +  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
     3.9  
    3.10  end;
     4.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 17:17:51 2014 +0200
     4.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 20:43:19 2014 +0200
     4.3 @@ -7,6 +7,12 @@
     4.4  type local_theory = Proof.context;
     4.5  type generic_theory = Context.generic;
     4.6  
     4.7 +structure Attrib =
     4.8 +struct
     4.9 +  type src = Args.src;
    4.10 +  type binding = binding * src list;
    4.11 +end;
    4.12 +
    4.13  signature LOCAL_THEORY =
    4.14  sig
    4.15    type operations
    4.16 @@ -14,6 +20,7 @@
    4.17    val restore: local_theory -> local_theory
    4.18    val level: Proof.context -> int
    4.19    val assert_bottom: bool -> local_theory -> local_theory
    4.20 +  val mark_brittle: local_theory -> local_theory
    4.21    val assert_nonbrittle: local_theory -> local_theory
    4.22    val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
    4.23      local_theory -> local_theory
    4.24 @@ -52,16 +59,13 @@
    4.25    val subscription: string * morphism -> (morphism * bool) option -> morphism ->
    4.26      local_theory -> local_theory
    4.27    val pretty: local_theory -> Pretty.T list
    4.28 +  val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
    4.29    val set_defsort: sort -> local_theory -> local_theory
    4.30    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
    4.31    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    4.32    val class_alias: binding -> class -> local_theory -> local_theory
    4.33    val type_alias: binding -> string -> local_theory -> local_theory
    4.34    val const_alias: binding -> string -> local_theory -> local_theory
    4.35 -  val activate: string * morphism -> (morphism * bool) option -> morphism ->
    4.36 -    local_theory -> local_theory
    4.37 -  val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
    4.38 -    local_theory -> local_theory
    4.39    val init: Name_Space.naming -> operations -> Proof.context -> local_theory
    4.40    val exit: local_theory -> Proof.context
    4.41    val exit_global: local_theory -> theory
    4.42 @@ -115,7 +119,7 @@
    4.43  val bottom_of = List.last o Data.get o assert;
    4.44  val top_of = hd o Data.get o assert;
    4.45  
    4.46 -fun map_bottom f =
    4.47 +fun map_top f =
    4.48    assert #>
    4.49    Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
    4.50      make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
    4.51 @@ -162,14 +166,13 @@
    4.52  (* brittle context -- implicit for nested structures *)
    4.53  
    4.54  fun mark_brittle lthy =
    4.55 -  if level lthy = 1
    4.56 -  then map_bottom (fn (naming, operations, after_close, brittle, target) =>
    4.57 -    (naming, operations, after_close, true, target)) lthy
    4.58 +  if level lthy = 1 then
    4.59 +    map_top (fn (naming, operations, after_close, brittle, target) =>
    4.60 +      (naming, operations, after_close, true, target)) lthy
    4.61    else lthy;
    4.62  
    4.63  fun assert_nonbrittle lthy =
    4.64 -  if #brittle (top_of lthy)
    4.65 -  then error "Brittle local theory context"
    4.66 +  if #brittle (top_of lthy) then error "Brittle local theory context"
    4.67    else lthy;
    4.68  
    4.69  
    4.70 @@ -179,7 +182,7 @@
    4.71  val full_name = Name_Space.full_name o naming_of;
    4.72  
    4.73  fun map_naming f =
    4.74 -  map_bottom (fn (naming, operations, after_close, brittle, target) =>
    4.75 +  map_top (fn (naming, operations, after_close, brittle, target) =>
    4.76      (f naming, operations, after_close, brittle, target));
    4.77  
    4.78  val conceal = map_naming Name_Space.conceal;
    4.79 @@ -272,6 +275,20 @@
    4.80  val notes = notes_kind "";
    4.81  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    4.82  
    4.83 +fun add_thms_dynamic (binding, f) lthy =
    4.84 +  lthy
    4.85 +  |> background_theory_result (fn thy => thy
    4.86 +      |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f))
    4.87 +  |-> (fn name =>
    4.88 +    map_contexts (fn _ => fn ctxt =>
    4.89 +      Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
    4.90 +    declaration {syntax = false, pervasive = false} (fn phi =>
    4.91 +      let val binding' = Morphism.binding phi binding in
    4.92 +        Context.mapping
    4.93 +          (Global_Theory.alias_fact binding' name)
    4.94 +          (Proof_Context.fact_alias binding' name)
    4.95 +      end));
    4.96 +
    4.97  fun set_defsort S =
    4.98    declaration {syntax = true, pervasive = false}
    4.99      (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
   4.100 @@ -308,17 +325,6 @@
   4.101  val const_alias = alias Sign.const_alias Proof_Context.const_alias;
   4.102  
   4.103  
   4.104 -(* activation of locale fragments *)
   4.105 -
   4.106 -fun activate_nonbrittle dep_morph mixin export =
   4.107 -  map_bottom (fn (naming, operations, after_close, brittle, target) =>
   4.108 -    (naming, operations, after_close, brittle,
   4.109 -      (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
   4.110 -
   4.111 -fun activate dep_morph mixin export =
   4.112 -  mark_brittle #> activate_nonbrittle dep_morph mixin export;
   4.113 -
   4.114 -
   4.115  
   4.116  (** init and exit **)
   4.117  
     5.1 --- a/src/Pure/Isar/locale.ML	Wed Aug 13 17:17:51 2014 +0200
     5.2 +++ b/src/Pure/Isar/locale.ML	Wed Aug 13 20:43:19 2014 +0200
     5.3 @@ -70,6 +70,10 @@
     5.4    (* Registrations and dependencies *)
     5.5    val add_registration: string * morphism -> (morphism * bool) option ->
     5.6      morphism -> Context.generic -> Context.generic
     5.7 +  val activate_fragment: string * morphism -> (morphism * bool) option -> morphism ->
     5.8 +    local_theory -> local_theory
     5.9 +  val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
    5.10 +    local_theory -> local_theory
    5.11    val amend_registration: string * morphism -> morphism * bool ->
    5.12      morphism -> Context.generic -> Context.generic
    5.13    val registrations_of: Context.generic -> string -> (string * morphism) list
    5.14 @@ -514,6 +518,19 @@
    5.15    end;
    5.16  
    5.17  
    5.18 +(* locale fragments within local theory *)
    5.19 +
    5.20 +fun activate_fragment_nonbrittle dep_morph mixin export lthy =
    5.21 +  let val n = Local_Theory.level lthy in
    5.22 +    lthy |> Local_Theory.map_contexts (fn level =>
    5.23 +      level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export))
    5.24 +  end;
    5.25 +
    5.26 +fun activate_fragment dep_morph mixin export =
    5.27 +  Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export;
    5.28 +
    5.29 +
    5.30 +
    5.31  (*** Dependencies ***)
    5.32  
    5.33  (* FIXME dead code!?
     6.1 --- a/src/Pure/Isar/proof_context.ML	Wed Aug 13 17:17:51 2014 +0200
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Aug 13 20:43:19 2014 +0200
     6.3 @@ -50,6 +50,7 @@
     6.4    val markup_const: Proof.context -> string -> string
     6.5    val pretty_const: Proof.context -> string -> Pretty.T
     6.6    val transfer: theory -> Proof.context -> Proof.context
     6.7 +  val transfer_facts: theory -> Proof.context -> Proof.context
     6.8    val background_theory: (theory -> theory) -> Proof.context -> Proof.context
     6.9    val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
    6.10    val facts_of: Proof.context -> Facts.T
    6.11 @@ -323,16 +324,19 @@
    6.12    map_tsig (fn tsig as (local_tsig, global_tsig) =>
    6.13      let val thy_tsig = Sign.tsig_of thy in
    6.14        if Type.eq_tsig (thy_tsig, global_tsig) then tsig
    6.15 -      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
    6.16 +      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
    6.17      end) |>
    6.18    map_consts (fn consts as (local_consts, global_consts) =>
    6.19      let val thy_consts = Sign.consts_of thy in
    6.20        if Consts.eq_consts (thy_consts, global_consts) then consts
    6.21 -      else (Consts.merge (local_consts, thy_consts), thy_consts)
    6.22 +      else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
    6.23      end);
    6.24  
    6.25  fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
    6.26  
    6.27 +fun transfer_facts thy =
    6.28 +  map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts));
    6.29 +
    6.30  fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
    6.31  
    6.32  fun background_theory_result f ctxt =
     7.1 --- a/src/Pure/PIDE/prover.scala	Wed Aug 13 17:17:51 2014 +0200
     7.2 +++ b/src/Pure/PIDE/prover.scala	Wed Aug 13 20:43:19 2014 +0200
     7.3 @@ -1,7 +1,8 @@
     7.4  /*  Title:      Pure/PIDE/prover.scala
     7.5      Author:     Makarius
     7.6 +    Options:    :folding=explicit:
     7.7  
     7.8 -General prover operations and process wrapping.
     7.9 +Prover process wrapping.
    7.10  */
    7.11  
    7.12  package isabelle
    7.13 @@ -87,7 +88,7 @@
    7.14    system_channel: System_Channel,
    7.15    system_process: Prover.System_Process) extends Protocol
    7.16  {
    7.17 -  /* output */
    7.18 +  /** receiver output **/
    7.19  
    7.20    val xml_cache: XML.Cache = new XML.Cache()
    7.21  
     8.1 --- a/src/Pure/PIDE/session.scala	Wed Aug 13 17:17:51 2014 +0200
     8.2 +++ b/src/Pure/PIDE/session.scala	Wed Aug 13 20:43:19 2014 +0200
     8.3 @@ -1,6 +1,6 @@
     8.4  /*  Title:      Pure/PIDE/session.scala
     8.5      Author:     Makarius
     8.6 -    Options:    :folding=explicit:collapseFolds=1:
     8.7 +    Options:    :folding=explicit:
     8.8  
     8.9  PIDE editor session, potentially with running prover process.
    8.10  */
     9.1 --- a/src/Pure/ROOT.ML	Wed Aug 13 17:17:51 2014 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Wed Aug 13 20:43:19 2014 +0200
     9.3 @@ -234,7 +234,8 @@
     9.4  use "Isar/parse.ML";
     9.5  use "Isar/args.ML";
     9.6  
     9.7 -(*theory sources*)
     9.8 +(*theory specifications*)
     9.9 +use "Isar/local_theory.ML";
    9.10  use "Thy/thy_header.ML";
    9.11  use "PIDE/command_span.ML";
    9.12  use "Thy/thy_syntax.ML";
    9.13 @@ -264,7 +265,6 @@
    9.14  
    9.15  (*local theories and targets*)
    9.16  use "Isar/locale.ML";
    9.17 -use "Isar/local_theory.ML";
    9.18  use "Isar/generic_target.ML";
    9.19  use "Isar/overloading.ML";
    9.20  use "axclass.ML";
    10.1 --- a/src/Pure/Tools/build.scala	Wed Aug 13 17:17:51 2014 +0200
    10.2 +++ b/src/Pure/Tools/build.scala	Wed Aug 13 20:43:19 2014 +0200
    10.3 @@ -1,6 +1,6 @@
    10.4  /*  Title:      Pure/Tools/build.scala
    10.5      Author:     Makarius
    10.6 -    Options:    :folding=explicit:collapseFolds=1:
    10.7 +    Options:    :folding=explicit:
    10.8  
    10.9  Build and manage Isabelle sessions.
   10.10  */
    11.1 --- a/src/Pure/Tools/named_theorems.ML	Wed Aug 13 17:17:51 2014 +0200
    11.2 +++ b/src/Pure/Tools/named_theorems.ML	Wed Aug 13 20:43:19 2014 +0200
    11.3 @@ -65,22 +65,10 @@
    11.4      val description =
    11.5        "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
    11.6      val lthy' = lthy
    11.7 -      |> Local_Theory.background_theory
    11.8 -        (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #>
    11.9 -         Attrib.setup binding (Attrib.add_del (add name) (del name)) description #>
   11.10 -         Context.theory_map (new_entry name))
   11.11 +      |> Local_Theory.background_theory (Context.theory_map (new_entry name))
   11.12        |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
   11.13 -      |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
   11.14 -          let
   11.15 -            val binding' = Morphism.binding phi binding;
   11.16 -            val context' =
   11.17 -              context |> Context.mapping
   11.18 -                (Global_Theory.alias_fact binding' name)
   11.19 -                (fn ctxt =>
   11.20 -                  if Facts.defined (Proof_Context.facts_of ctxt) name
   11.21 -                  then Proof_Context.fact_alias binding' name ctxt
   11.22 -                  else ctxt);
   11.23 -          in context' end);
   11.24 +      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
   11.25 +      |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
   11.26    in (name, lthy') end;
   11.27  
   11.28  val _ =
    12.1 --- a/src/Pure/global_theory.ML	Wed Aug 13 17:17:51 2014 +0200
    12.2 +++ b/src/Pure/global_theory.ML	Wed Aug 13 20:43:19 2014 +0200
    12.3 @@ -29,6 +29,8 @@
    12.4    val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
    12.5    val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
    12.6    val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
    12.7 +  val add_thms_dynamic': Context.generic -> binding * (Context.generic -> thm list) ->
    12.8 +    theory -> string * theory
    12.9    val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   12.10    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
   12.11      -> theory -> (string * thm list) list * theory
   12.12 @@ -157,10 +159,14 @@
   12.13  val add_thm = yield_singleton add_thms;
   12.14  
   12.15  
   12.16 -(* add_thms_dynamic *)
   12.17 +(* dynamic theorems *)
   12.18  
   12.19 -fun add_thms_dynamic (b, f) thy = thy
   12.20 -  |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
   12.21 +fun add_thms_dynamic' context arg thy =
   12.22 +  let val (name, facts') = Facts.add_dynamic context arg (Data.get thy)
   12.23 +  in (name, Data.put facts' thy) end;
   12.24 +
   12.25 +fun add_thms_dynamic arg thy =
   12.26 +  add_thms_dynamic' (Context.Theory thy) arg thy |> snd;
   12.27  
   12.28  
   12.29  (* note_thmss *)