diff -r f745ff8bdb91 -r 9cb51c2358ea datatype.ML
--- a/datatype.ML	Thu Sep 08 11:01:45 1994 +0200
+++ b/datatype.ML	Sun Sep 11 10:31:17 1994 +0200
@@ -95,13 +95,13 @@
 val primrec_decl =
   let fun mkstrings((fname,tname),axms) =
     let fun prove (name,eqn) =
-      "val "^name^"= prove_goalw thy [get_def thy \""^fname^"\"] "
+      "val "^name^"= prove_goalw thy [get_def thy "^fname^"] "
       ^ eqn ^"\n\
        \(fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])"
     in ("|> " ^ tname^"_add_primrec " ^ mk_list (map snd axms)
 	, cat_lines(map prove axms))
     end
-  in ident -- long_id -- repeat1 (ident -- string)  >> mkstrings end
+  in name -- long_id -- repeat1 (ident -- string)  >> mkstrings end
 end;
 
 (*used for constructor parameters*)