diff -r c57ab3ce997e -r a0e6613dfbee Datatype.ML
--- a/Datatype.ML	Mon Aug 15 15:20:34 1994 +0200
+++ b/Datatype.ML	Tue Aug 16 09:57:51 1994 +0200
@@ -94,7 +94,7 @@
         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;