src/Pure/drule.ML
changeset 7404 e488cf3da60a
parent 7380 2bcee6a460d8
child 7467 71e5d8671e7b
     1.1 --- a/src/Pure/drule.ML	Wed Sep 01 11:16:02 1999 +0200
     1.2 +++ b/src/Pure/drule.ML	Wed Sep 01 21:04:01 1999 +0200
     1.3 @@ -429,7 +429,7 @@
     1.4  
     1.5  fun read_prop s = read_cterm proto_sign (s, propT);
     1.6  
     1.7 -fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
     1.8 +fun store_thm name thm = hd (PureThy.smart_store_thms (name, [standard thm]));
     1.9  
    1.10  val reflexive_thm =
    1.11    let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))