Now recdef checks the name of the function being defined.
authorpaulson
Mon May 26 12:42:38 1997 +0200 (1997-05-26)
changeset 33454d888ddd6284
parent 3344 b3e39a2987c1
child 3346 5101517c2614
Now recdef checks the name of the function being defined.
Slight tidying
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Mon May 26 12:40:51 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon May 26 12:42:38 1997 +0200
     1.3 @@ -238,6 +238,7 @@
     1.4  	 (";\n\n\
     1.5            \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
     1.6            \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
     1.7 +	                 quote fid ^ " " ^ 
     1.8  	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
     1.9            \val thy = thy"
    1.10           ,
    1.11 @@ -245,8 +246,8 @@
    1.12            \  struct\n\
    1.13            \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
    1.14            \  val {rules, induct, tcs} = \n\
    1.15 -          \    \t Tfl.simplify_defn(thy, (\"" ^ fid ^ 
    1.16 -					  "\", pats_" ^ intrnl_name ^ "))\n\
    1.17 +          \    \t Tfl.simplify_defn(thy, (" ^ quote fid ^ 
    1.18 +					  ", pats_" ^ intrnl_name ^ "))\n\
    1.19            \  end;\n\
    1.20            \val pats_" ^ intrnl_name ^ " = ();\n")
    1.21    end;