src/Pure/drule.ML
changeset 7404 e488cf3da60a
parent 7380 2bcee6a460d8
child 7467 71e5d8671e7b
--- 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)))