
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 \<times> code_numeral"
+type_synonym seed = "code_numeral \<times> code_numeral"
 
 primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
   "next (v, w) = (let




