# HG changeset patch
# User haftmann
# Date 1202283291 -3600
# Node ID e7a421d1f5c1f40660abae8d20247d38a2b972c7
# Parent  c2e15e65165f2a446110f927e539869f50096884
continued

diff -r c2e15e65165f -r e7a421d1f5c1 src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Wed Feb 06 08:34:32 2008 +0100
+++ b/src/HOL/ex/Random.thy	Wed Feb 06 08:34:51 2008 +0100
@@ -195,8 +195,8 @@
 
 subsection {* The @{text random} class *}
 
-class random = type +
-  fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
+class random =
+  fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a\<Colon>{} \<times> seed"
 
 -- {* FIXME dummy implementations *}
 
@@ -230,7 +230,7 @@
 
 end
 
-instantiation "+" :: (random, random) random
+instantiation "+" :: ("{type, random}", "{type, random}") random
 begin
 
 definition
@@ -250,7 +250,7 @@
 
 end
 
-instantiation "*" :: (random, random) random
+instantiation "*" :: ("{type, random}", "{type, random}") random
 begin
 
 definition
@@ -277,7 +277,7 @@
 
 end
 
-instantiation list :: (random) random
+instantiation list :: ("{type, random}") random
 begin
 
 primrec
@@ -429,7 +429,7 @@
 code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
   (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
 
-instantiation "fun" :: (eq, random) random
+instantiation "fun" :: (eq, "{type, random}") random
 begin
 
 definition