src/HOL/thy_syntax.ML

--- a/src/HOL/thy_syntax.ML	Tue May 04 13:47:28 1999 +0200
+++ b/src/HOL/thy_syntax.ML	Tue May 04 16:18:16 1999 +0200
@@ -217,7 +217,7 @@
   let
     val fid = strip_quotes fname;
     val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
-    val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms);
+    val axms_text = mk_big_list axms;
   in
     ";\n\n\
     \local\n\