src/Pure/Thy/thm_database.ML

 
 (* store in theory and generate HTML *)
 
 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 *)
 
 val qed_thm: thm option ref = ref None;