src/HOL/thy_syntax.ML
changeset 6576 7e0b35bed503
parent 6555 17b7b88a8e3c
child 6642 732af87c0650
     1.1 --- a/src/HOL/thy_syntax.ML	Tue May 04 13:47:28 1999 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Tue May 04 16:18:16 1999 +0200
     1.3 @@ -217,7 +217,7 @@
     1.4    let
     1.5      val fid = strip_quotes fname;
     1.6      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
     1.7 -    val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms);
     1.8 +    val axms_text = mk_big_list axms;
     1.9    in
    1.10      ";\n\n\
    1.11      \local\n\