# HG changeset patch
# User nipkow
# Date 777023871 -7200
# Node ID a0e6613dfbeeeb9796252c478485639a73b1ef3a
# Parent  c57ab3ce997e0a88f70077eb1fd0cc643085c186
allow long_id for reference to type in primrec.
Doesn't work yet, though, because of problems with the autoloader.

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;