# HG changeset patch
# User wenzelm
# Date 939135313 -7200
# Node ID e17ccb79db68b92663f8dd5eae172915eed78c92
# Parent  acaf55bee03e4ac99b1779d6a49c3a2b27382c74
fixed ml_store_thm(s): deriv;

diff -r acaf55bee03e -r e17ccb79db68 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Tue Oct 05 15:42:44 1999 +0200
+++ b/src/Pure/Thy/thm_database.ML	Tue Oct 05 16:55:13 1999 +0200
@@ -71,13 +71,13 @@
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in
     if warn_ml name then ()
-    else (qed_thms := [thm]; use_text true ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
+    else (qed_thms := [thm']; use_text true ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
   end;
 
 fun ml_store_thms (name, thms) =
   let val thms' = store_thms (name, thms) in
     if warn_ml name then ()
-    else (qed_thms := thms; use_text true ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
+    else (qed_thms := thms'; use_text true ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
   end;
 
 fun bind_thm (name, thm) = ml_store_thm (name, standard thm);