src/Pure/Thy/thm_database.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5155 21177b8a4d7f
--- a/src/Pure/Thy/thm_database.ML	Fri Jun 26 15:16:14 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML	Mon Jun 29 10:32:06 1998 +0200
@@ -52,7 +52,7 @@
   let val thm' = store_thm (name, thm) in
     if is_ml_identifier name then
       (qed_thm := Some thm';
-        use_text ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
+        use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
     else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
   end;