# HG changeset patch
# User blanchet
# Date 1410947699 -7200
# Node ID a416218a3a11b3c5fdab985522193d1a42d8bfea
# Parent  2f04f1fd28aab387014017bee719dce2143190b2
avoid clash with Quickcheck's generated 'random_xxx' function

diff -r 2f04f1fd28aa -r a416218a3a11 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 17 11:12:46 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 17 11:54:59 2014 +0200
@@ -1997,7 +1997,7 @@
 pseudorandom seed (@{text n}):
 *}
 
-    primcorec
+    primcorec(*<*) (in early)(*>*)
       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
     where
       "random_process s f n =