# HG changeset patch
# User wenzelm
# Date 877964270 -3600
# Node ID 6adc18bd00093ae44999e276b59f1feda9f7dca5
# Parent  c161162bc8c593d47ad45daee8d5b70d321e02dc
renamed put_* to store_*;

diff -r c161162bc8c5 -r 6adc18bd0009 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Oct 27 15:43:53 1997 +0100
+++ b/src/Pure/pure_thy.ML	Mon Oct 27 15:57:50 1997 +0100
@@ -7,9 +7,10 @@
 
 signature PURE_THY =
 sig
-  val put_thms: (bstring * thm) list -> theory -> theory        (*DESTRUCTIVE*)
-  val put_thmss: (bstring * thm list) list -> theory -> theory  (*DESTRUCTIVE*)
-  val store_thm: (bstring * thm) -> thm                         (*DESTRUCTIVE*)
+  val store_thms: (bstring * thm) list -> theory -> theory   	  (*DESTRUCTIVE*)
+  val store_thmss: (bstring * thm list) list -> theory -> theory  (*DESTRUCTIVE*)
+  val store_thm: theory -> (bstring * thm) -> thm                 (*DESTRUCTIVE*)
+  val smart_store_thm: (bstring * thm) -> thm                     (*DESTRUCTIVE*)
   val get_thm: theory -> xstring -> thm
   val get_thms: theory -> xstring -> thm list
   val proto_pure: theory
@@ -144,13 +145,13 @@
   (enter_thms sg single name_thms; ());
 
 
-fun put_thmss thmss thy =
+fun store_thmss thmss thy =
   (seq (do_enter_thms (sign_of thy) false) thmss; thy);
 
-fun put_thms thms thy =
+fun store_thms thms thy =
   (seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy);
 
-fun store_thm (name, thm) =
+fun smart_store_thm (name, thm) =
   let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm])
   in named_thm end;