diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Random.thy --- a/src/HOL/Random.thy Wed Mar 30 11:32:51 2011 +0200 +++ b/src/HOL/Random.thy Wed Mar 30 11:32:52 2011 +0200 @@ -25,7 +25,7 @@ subsection {* Random seeds *} -types seed = "code_numeral \ code_numeral" +type_synonym seed = "code_numeral \ code_numeral" primrec "next" :: "seed \ code_numeral \ seed" where "next (v, w) = (let