# HG changeset patch
# User wenzelm
# Date 1206814450 -3600
# Node ID b497e3187ec72a6a23c24c38c882da85006544f8
# Parent  49850ac120e312ced4dcc6f8db80d44fc90b0dde
eliminated destructive/critical theorem database;
simplified store_thm(s);
removed obsolete smart_store_thm(s);
tuned;

diff -r 49850ac120e3 -r b497e3187ec7 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Mar 29 19:14:09 2008 +0100
+++ b/src/Pure/pure_thy.ML	Sat Mar 29 19:14:10 2008 +0100
@@ -41,14 +41,12 @@
   val name_thm: bool -> bool -> string -> thm -> thm
   val name_thms: bool -> bool -> string -> thm list -> thm list
   val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
-  val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory
-  val smart_store_thms: (bstring * thm list) -> thm list
-  val smart_store_thms_open: (bstring * thm list) -> thm list
-  val forall_elim_var: int -> thm -> thm
-  val forall_elim_vars: int -> thm -> thm
-  val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
+  val store_thms: bstring * thm list -> theory -> thm list * theory
+  val store_thm: bstring * thm -> theory -> thm * theory
+  val store_thm_open: bstring * thm -> theory -> thm * theory
   val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
+  val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
   val note: string -> string * thm -> theory -> thm * theory
   val note_thmss: string -> ((bstring * attribute list) *
     (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
@@ -58,6 +56,8 @@
     (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   val note_thmss_qualified: string -> string -> ((bstring * attribute list) *
     (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
+  val forall_elim_var: int -> thm -> thm
+  val forall_elim_vars: int -> thm -> thm
   val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
   val add_axiomss: ((bstring * string list) * attribute list) list ->
@@ -132,24 +132,24 @@
  {theorems: thm list NameSpace.table,   (* FIXME legacy *)
   all_facts: Facts.T};
 
-fun make_thms theorems all_facts = Thms {theorems = theorems, all_facts = all_facts};
+fun make_thms (theorems, all_facts) = Thms {theorems = theorems, all_facts = all_facts};
 
 structure TheoremsData = TheoryDataFun
 (
-  type T = thms ref;   (* FIXME legacy *)
-  val empty = ref (make_thms NameSpace.empty_table Facts.empty);
-  fun copy (ref x) = ref x;
-  fun extend (ref (Thms {theorems = _, all_facts})) = ref (make_thms NameSpace.empty_table all_facts);
+  type T = thms;
+  val empty = make_thms (NameSpace.empty_table, Facts.empty);
+  val copy = I;
+  fun extend (Thms {theorems = _, all_facts}) = make_thms (NameSpace.empty_table, all_facts);
   fun merge _
-     (ref (Thms {theorems = _, all_facts = all_facts1}),
-      ref (Thms {theorems = _, all_facts = all_facts2})) =
-    ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2)));
+     (Thms {theorems = _, all_facts = all_facts1},
+      Thms {theorems = _, all_facts = all_facts2}) =
+    make_thms (NameSpace.empty_table, Facts.merge (all_facts1, all_facts2));
 );
 
-val _ = Context.>> (Context.map_theory TheoremsData.init);
+fun map_theorems f =
+  TheoremsData.map (fn Thms {theorems, all_facts} => make_thms (f (theorems, all_facts)));
 
-val get_theorems_ref = TheoremsData.get;
-val get_theorems = (fn Thms args => args) o ! o get_theorems_ref;
+val get_theorems = (fn Thms args => args) o TheoremsData.get;
 val theorems_of = #theorems o get_theorems;
 val all_facts_of = #all_facts o get_theorems;
 
@@ -180,6 +180,7 @@
     val pos = Facts.pos_of_ref thmref;
     val new_res = lookup_fact theory name;
     val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
+    val _ = Theory.check_thy theory;
     val is_same =
       (case (new_res, old_res) of
         (NONE, NONE) => true
@@ -216,15 +217,14 @@
 
 
 
-(** store theorems **)                    (*DESTRUCTIVE*)
+(** store theorems **)
 
 (* hiding -- affects current theory node only *)
 
-fun hide_thms fully names thy = NAMED_CRITICAL "thm" (fn () =>
-  let
-    val r as ref (Thms {theorems = (space, thms), all_facts}) = get_theorems_ref thy;
-    val space' = fold (NameSpace.hide fully) names space;
-  in r := make_thms (space', thms) all_facts; thy end);
+fun hide_thms fully names =
+  map_theorems (fn ((space, thms), all_facts) =>
+    let val space' = fold (NameSpace.hide fully) names space
+    in ((space', thms), all_facts) end);
 
 
 (* fact specifications *)
@@ -252,40 +252,31 @@
   burrow_fact (name_thms true official name) fact;
 
 
-(* add_thms_dynamic *)
-
-fun add_thms_dynamic (bname, f) thy = NAMED_CRITICAL "thm" (fn () =>
-  let
-    val name = Sign.full_name thy bname;
-    val r as ref (Thms {theorems, all_facts}) = get_theorems_ref thy;
-    val all_facts' = Facts.add_dynamic (Sign.naming_of thy) (name, f) all_facts;
-    val _ = r := make_thms theorems all_facts';
-  in thy end);
-
-
 (* enter_thms *)
 
-fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
-fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
-
 fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap
-  | enter_thms pre_name post_name app_att (bname, thms) thy = NAMED_CRITICAL "thm" (fn () =>
+  | enter_thms pre_name post_name app_att (bname, thms) thy =
       let
-        val name = Sign.full_name thy bname;
+        val naming = Sign.naming_of thy;
+        val name = NameSpace.full naming bname;
         val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
-        val r as ref (Thms {theorems = (space, theorems), all_facts}) = get_theorems_ref thy';
-        val space' = Sign.declare_name thy' name space;
-        val theorems' = Symtab.update (name, thms') theorems;
-        val all_facts' = Facts.add_global (Sign.naming_of thy') (name, thms') all_facts;
-      in
-        (case Symtab.lookup theorems name of
-          NONE => ()
-        | SOME thms'' =>
-            if Thm.eq_thms (thms', thms'') then warn_same name
-            else warn_overwrite name);
-        r := make_thms (space', theorems') all_facts';
-        (thms', thy')
-      end);
+        val thms'' = map (Thm.transfer thy') thms';
+        val thy'' = thy' |> map_theorems (fn ((space, theorems), all_facts) =>
+          let
+            val space' = NameSpace.declare naming name space;
+            val theorems' = Symtab.update (name, thms'') theorems;
+            val all_facts' = Facts.add_global naming (name, thms'') all_facts;
+          in ((space', theorems'), all_facts') end);
+      in (thms'', thy'') end;
+
+
+(* store_thm(s) *)
+
+val store_thms = enter_thms (name_thms true true) (name_thms false true) I;
+fun store_thm (name, th) = store_thms (name, [th]) #>> the_single;
+
+fun store_thm_open (name, th) =
+  enter_thms (name_thms true false) (name_thms false false) I (name, [th]) #>> the_single;
 
 
 (* add_thms(s) *)
@@ -304,6 +295,16 @@
 val add_thms = gen_add_thms (name_thms true true);
 
 
+(* add_thms_dynamic *)
+
+fun add_thms_dynamic (bname, f) thy =
+  let
+    val name = Sign.full_name thy bname;
+    val thy' = thy |> map_theorems (fn (theorems, all_facts) =>
+      (theorems, Facts.add_dynamic (Sign.naming_of thy) (name, f) all_facts));
+  in thy' end;
+
+
 (* note_thmss(_i) *)
 
 local
@@ -336,35 +337,6 @@
   ||> Sign.restore_naming thy;
 
 
-(* store_thm *)
-
-fun store_thm ((bname, thm), atts) thy =
-  let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy
-  in (th', thy') end;
-
-
-(* smart_store_thms(_open) *)
-
-local
-
-fun smart_store _ (name, []) =
-      error ("Cannot store empty list of theorems: " ^ quote name)
-  | smart_store official (name, [thm]) =
-      fst (enter_thms (name_thms true official) (name_thms false official) I (name, [thm])
-        (Thm.theory_of_thm thm))
-  | smart_store official (name, thms) =
-      let val thy = Theory.merge_list (map Thm.theory_of_thm thms) in
-        fst (enter_thms (name_thms true official) (name_thms false official) I (name, thms) thy)
-      end;
-
-in
-
-val smart_store_thms = smart_store true;
-val smart_store_thms_open = smart_store false;
-
-end;
-
-
 (* forall_elim_var(s) -- belongs to drule.ML *)
 
 fun forall_elim_vars_aux strip_vars i th =