diff -r 956d6acacf89 -r 1fbd4aba46e3 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Jan 24 17:56:18 2005 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Jan 24 17:59:48 2005 +0100
@@ -523,7 +523,7 @@
 
 (* standard sections *)
 
-fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";";
+fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", None);";
 val mk_vals = cat_lines o map mk_val;
 
 fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)