1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 25 19:39:58 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 25 19:39:59 2008 +0100
     1.3 @@ -811,7 +811,7 @@
     1.4          val thms =
     1.5            if name = "" then [Thm.transfer thy Drule.dummy_thm]
     1.6            else
     1.7 -            (case Facts.lookup local_facts name of
     1.8 +            (case Facts.lookup (Context.Proof ctxt) local_facts name of
     1.9                SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
    1.10              | NONE => from_thy thy xthmref);
    1.11        in pick name thms end;

     2.1 --- a/src/Pure/facts.ML	Tue Mar 25 19:39:58 2008 +0100
     2.2 +++ b/src/Pure/facts.ML	Tue Mar 25 19:39:59 2008 +0100
     2.3 @@ -20,17 +20,18 @@
     2.4    val select: ref -> thm list -> thm list
     2.5    val selections: string * thm list -> (ref * thm) list
     2.6    type T
     2.7 +  val empty: T
     2.8    val space_of: T -> NameSpace.T
     2.9 -  val lookup: T -> string -> thm list option
    2.10 +  val lookup: Context.generic -> T -> string -> thm list option
    2.11    val dest: T -> (string * thm list) list
    2.12    val extern: T -> (xstring * thm list) list
    2.13    val props: T -> thm list
    2.14    val could_unify: T -> term -> thm list
    2.15 -  val empty: T
    2.16    val merge: T * T -> T
    2.17 +  val del: string -> T -> T
    2.18    val add_global: NameSpace.naming -> string * thm list -> T -> T
    2.19    val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
    2.20 -  val del: string -> T -> T
    2.21 +  val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
    2.22  end;
    2.23  
    2.24  structure Facts: FACTS =
    2.25 @@ -112,13 +113,16 @@
    2.26  
    2.27  (** fact environment **)
    2.28  
    2.29 -(* datatype T *)
    2.30 +(* datatypes *)
    2.31 +
    2.32 +datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
    2.33  
    2.34  datatype T = Facts of
    2.35 - {facts: thm list NameSpace.table,
    2.36 + {facts: (fact * serial) NameSpace.table,
    2.37    props: thm Net.net};
    2.38  
    2.39  fun make_facts facts props = Facts {facts = facts, props = props};
    2.40 +val empty = make_facts NameSpace.empty_table Net.empty;
    2.41  
    2.42  
    2.43  (* named facts *)
    2.44 @@ -126,9 +130,21 @@
    2.45  fun facts_of (Facts {facts, ...}) = facts;
    2.46  
    2.47  val space_of = #1 o facts_of;
    2.48 -val lookup = Symtab.lookup o #2 o facts_of;
    2.49 -val dest = NameSpace.dest_table o facts_of;
    2.50 -val extern = NameSpace.extern_table o facts_of;
    2.51 +val table_of = #2 o facts_of;
    2.52 +
    2.53 +fun lookup context facts name =
    2.54 +  (case Symtab.lookup (table_of facts) name of
    2.55 +    NONE => NONE
    2.56 +  | SOME (Static ths, _) => SOME ths
    2.57 +  | SOME (Dynamic f, _) => SOME (f context));
    2.58 +
    2.59 +fun dest facts =
    2.60 +  Symtab.fold (fn (name, (Static ths, _)) => cons (name, ths) | _ => I) (table_of facts) [];
    2.61 +
    2.62 +fun extern facts =
    2.63 +  dest facts
    2.64 +  |> map (apfst (NameSpace.extern (space_of facts)))
    2.65 +  |> sort_wrt #1;
    2.66  
    2.67  
    2.68  (* indexed props *)
    2.69 @@ -139,16 +155,28 @@
    2.70  fun could_unify (Facts {props, ...}) = Net.unify_term props;
    2.71  
    2.72  
    2.73 -(* build facts *)
    2.74 +(* merge facts *)
    2.75  
    2.76 -val empty = make_facts NameSpace.empty_table Net.empty;
    2.77 +fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
    2.78  
    2.79  fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
    2.80    let
    2.81 -    val facts' = NameSpace.merge_tables (K true) (facts1, facts2);
    2.82 +    (* FIXME authentic version
    2.83 +    val facts' = NameSpace.merge_tables (eq_snd (op =)) (facts1, facts2)
    2.84 +      handle Symtab.DUP dup => err_dup_fact dup; *)
    2.85 +    val facts' = NameSpace.merge_tables (K true) (facts1, facts2)
    2.86      val props' = Net.merge (is_equal o prop_ord) (props1, props2);
    2.87    in make_facts facts' props' end;
    2.88  
    2.89 +
    2.90 +(* static entries *)
    2.91 +
    2.92 +fun del name (Facts {facts = (space, tab), props}) =
    2.93 +  let
    2.94 +    val space' = NameSpace.hide true name space handle ERROR _ => space;
    2.95 +    val tab' = Symtab.delete_safe name tab;
    2.96 +  in make_facts (space', tab') props end;
    2.97 +
    2.98  fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
    2.99    let
   2.100      val facts' =
   2.101 @@ -157,7 +185,8 @@
   2.102          let
   2.103            val (space, tab) = facts;
   2.104            val space' = NameSpace.declare naming name space;
   2.105 -          val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab
   2.106 +          val entry = (name, (Static ths, serial ()));
   2.107 +          val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   2.108              handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
   2.109                Position.str_of (Position.thread_data ())); tab);
   2.110          in (space', tab') end;
   2.111 @@ -169,10 +198,15 @@
   2.112  val add_global = add false false;
   2.113  val add_local = add true;
   2.114  
   2.115 -fun del name (Facts {facts = (space, tab), props}) =
   2.116 +
   2.117 +(* dynamic entries *)
   2.118 +
   2.119 +fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
   2.120    let
   2.121 -    val space' = NameSpace.hide true name space handle ERROR _ => space;
   2.122 -    val tab' = Symtab.delete_safe name tab;
   2.123 +    val space' = NameSpace.declare naming name space;
   2.124 +    val entry = (name, (Dynamic f, serial ()));
   2.125 +    val tab' = Symtab.update_new entry tab
   2.126 +      handle Symtab.DUP dup => err_dup_fact dup;
   2.127    in make_facts (space', tab') props end;
   2.128  
   2.129  end;

     3.1 --- a/src/Pure/pure_thy.ML	Tue Mar 25 19:39:58 2008 +0100
     3.2 +++ b/src/Pure/pure_thy.ML	Tue Mar 25 19:39:59 2008 +0100
     3.3 @@ -58,6 +58,7 @@
     3.4    val smart_store_thms_open: (bstring * thm list) -> thm list
     3.5    val forall_elim_var: int -> thm -> thm
     3.6    val forall_elim_vars: int -> thm -> thm
     3.7 +  val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
     3.8    val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
     3.9    val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
    3.10    val note: string -> string * thm -> theory -> thm * theory
    3.11 @@ -180,7 +181,7 @@
    3.12    let
    3.13      val facts = all_facts_of thy;
    3.14      val name = NameSpace.intern (Facts.space_of facts) xname;
    3.15 -  in Option.map (pair name) (Facts.lookup facts name) end;
    3.16 +  in Option.map (pair name) (Facts.lookup (Context.Theory thy) facts name) end;
    3.17  
    3.18  fun show_result NONE = "none"
    3.19    | show_result (SOME (name, _)) = quote name;
    3.20 @@ -265,6 +266,17 @@
    3.21    burrow_fact (name_thms true official name) fact;
    3.22  
    3.23  
    3.24 +(* add_thms_dynamic *)
    3.25 +
    3.26 +fun add_thms_dynamic (bname, f) thy = CRITICAL (fn () =>
    3.27 +  let
    3.28 +    val name = Sign.full_name thy bname;
    3.29 +    val r as ref (Thms {theorems, all_facts}) = get_theorems_ref thy;
    3.30 +    val all_facts' = Facts.add_dynamic (Sign.naming_of thy) (name, f) all_facts;
    3.31 +    val _ = r := make_thms theorems all_facts';
    3.32 +  in thy end);
    3.33 +
    3.34 +
    3.35  (* enter_thms *)
    3.36  
    3.37  fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
    3.38 @@ -544,3 +556,4 @@
    3.39  
    3.40  structure BasicPureThy: BASIC_PURE_THY = PureThy;
    3.41  open BasicPureThy;
    3.42 +