| changeset 29823 | 0ab754d13ccd |
| parent 29808 | b8b9d529663b |
| child 30945 | 0418e9bffbba |
--- a/src/HOL/Library/Quickcheck.thy Fri Feb 06 15:15:27 2009 +0100 +++ b/src/HOL/Library/Quickcheck.thy Fri Feb 06 15:15:32 2009 +0100 @@ -17,7 +17,7 @@ begin definition - "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))" + "random _ = Pair (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))" instance ..