src/HOL/thy_syntax.ML
changeset 3345 4d888ddd6284
parent 3308 da002cef7090
child 3403 6cc663f6d62e
--- 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;