Datatype.ML

                  ^ eqn ^"\n\
              \(fn _ => [resolve_tac " ^ tname^".recs 1])"
         in ("|> " ^ tname^"_add_primrec " ^ mk_list (map snd axms),
             cat_lines(map prove axms))
         end
-  in ident -- ident -- repeat1 (ident -- string)  >> mkstrings end
+  in ident -- long_id -- repeat1 (ident -- string)  >> mkstrings end
 
 end;
 
 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |