# HG changeset patch
# User wenzelm
# Date 1449568148 -3600
# Node ID 1530a0f195394f00edeaf8365770ff170b438006
# Parent  fc1556774cfe1f8c2a358d082142abae9839fd88
added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;

diff -r fc1556774cfe -r 1530a0f19539 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Dec 07 20:19:59 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Dec 08 10:49:08 2015 +0100
@@ -123,6 +123,8 @@
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
+  val add_thms_dynamic: binding * (Context.generic -> thm list) ->
+    Proof.context -> string * Proof.context
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
@@ -234,9 +236,13 @@
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
-fun map_data f =
-  Data.map (fn Data {mode, syntax, tsig, consts, facts, cases} =>
-    make_data (f (mode, syntax, tsig, consts, facts, cases)));
+fun map_data_result f ctxt =
+  let
+    val Data {mode, syntax, tsig, consts, facts, cases} = Data.get ctxt;
+    val (res, data') = f (mode, syntax, tsig, consts, facts, cases) ||> make_data;
+  in (res, Data.put data' ctxt) end;
+
+fun map_data f = snd o map_data_result (pair () o f);
 
 fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
   (mode, syntax, tsig, consts, facts, cases));
@@ -264,9 +270,12 @@
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, tsig, f consts, facts, cases));
 
-fun map_facts f =
-  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
-    (mode, syntax, tsig, consts, f facts, cases));
+fun map_facts_result f =
+  map_data_result (fn (mode, syntax, tsig, consts, facts, cases) =>
+    let val (res, facts') = f facts
+    in (res, (mode, syntax, tsig, consts, facts', cases)) end);
+
+fun map_facts f = snd o map_facts_result (pair () o f);
 
 fun map_cases f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
@@ -991,6 +1000,9 @@
 
 (* facts *)
 
+fun add_thms_dynamic arg ctxt =
+  ctxt |> map_facts_result (Facts.add_dynamic (Context.Proof ctxt) arg);
+
 local
 
 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))