# HG changeset patch
# User wenzelm
# Date 920978260 -3600
# Node ID c6abb5884fed7040ba2ce949fcda48b2cfd3f1f0
# Parent  1b55802e2b599fb2dbe3d5d48da40049b637ddb1
Present.theorem;

diff -r 1b55802e2b59 -r c6abb5884fed src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Tue Mar 09 12:13:58 1999 +0100
+++ b/src/Pure/Thy/thm_database.ML	Tue Mar 09 12:17:40 1999 +0100
@@ -36,7 +36,7 @@
 
 fun store_thm (name, thm) =
   let val thm' = PureThy.smart_store_thm (name, thm)
-  in Present.thm name thm'; thm' end;
+  in Present.theorem name thm'; thm' end;
 
 
 (* store on ML toplevel *)