Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PureThy.smart_store_thms;
authorwenzelm
Wed, 01 Sep 1999 21:04:01 +0200
changeset 7404 e488cf3da60a
parent 7403 c318acb88251
child 7405 7e4e286a9931
PureThy.smart_store_thms;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- 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)))
isabelle