| changeset 6327 | c6abb5884fed |
| parent 6204 | c7ad5b27894f |
| child 7182 | 090723b5024d |
--- 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 *)