# HG changeset patch
# User paulson
# Date 864643358 -7200
# Node ID 4d888ddd6284147f2827f24e82b86b0495c7b33c
# Parent  b3e39a2987c193ad19e7a770a575a908cdba6740
Now recdef checks the name of the function being defined.
Slight tidying

diff -r b3e39a2987c1 -r 4d888ddd6284 src/HOL/thy_syntax.ML
--- 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;