# HG changeset patch
# User wenzelm
# Date 936212641 -7200
# Node ID e488cf3da60ae9119d9fa73e87189876e3f8216e
# Parent  c318acb8825135dd58d683fc8d52c96705b25e9a
PureThy.smart_store_thms;

diff -r c318acb88251 -r e488cf3da60a src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Sep 01 11:16:02 1999 +0200
+++ b/src/Pure/drule.ML	Wed Sep 01 21:04:01 1999 +0200
@@ -429,7 +429,7 @@
 
 fun read_prop s = read_cterm proto_sign (s, propT);
 
-fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
+fun store_thm name thm = hd (PureThy.smart_store_thms (name, [standard thm]));
 
 val reflexive_thm =
   let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))