--- a/src/HOL/thy_syntax.ML Mon May 26 12:40:51 1997 +0200
+++ b/src/HOL/thy_syntax.ML Mon May 26 12:42:38 1997 +0200
@@ -238,6 +238,7 @@
(";\n\n\
\val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
\val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^
+ quote fid ^ " " ^
rel ^ "\n" ^ mk_big_list axms ^ ";\n\
\val thy = thy"
,
@@ -245,8 +246,8 @@
\ struct\n\
\ val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
\ val {rules, induct, tcs} = \n\
- \ \t Tfl.simplify_defn(thy, (\"" ^ fid ^
- "\", pats_" ^ intrnl_name ^ "))\n\
+ \ \t Tfl.simplify_defn(thy, (" ^ quote fid ^
+ ", pats_" ^ intrnl_name ^ "))\n\
\ end;\n\
\val pats_" ^ intrnl_name ^ " = ();\n")
end;