datatype.ML

 end
 
 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*)
 datatype dt_type = dtVar of string |
   dtTyp of dt_type list * string |