1.1 --- a/src/HOL/ex/Quickcheck.thy	Tue Sep 16 09:21:22 2008 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck.thy	Tue Sep 16 09:21:24 2008 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* A simple counterexample generator *}
     1.5  
     1.6  theory Quickcheck
     1.7 -imports Random Eval
     1.8 +imports Random Code_Eval
     1.9  begin
    1.10  
    1.11  subsection {* The @{text random} class *}
    1.12 @@ -19,7 +19,7 @@
    1.13  begin
    1.14  
    1.15  definition
    1.16 -  "random _ = return (TYPE('a), \<lambda>u. Eval.Const (STR ''TYPE'') RTYPE('a))"
    1.17 +  "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') RTYPE('a))"
    1.18  
    1.19  instance ..
    1.20  
    1.21 @@ -173,9 +173,9 @@
    1.22    "random n = (do
    1.23       (b, _) \<leftarrow> random n;
    1.24       (m, t) \<leftarrow> random n;
    1.25 -     return (if b then (int m, \<lambda>u. Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))
    1.26 -       else (- int m, \<lambda>u. Eval.App (Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int))
    1.27 -         (Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))))
    1.28 +     return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))
    1.29 +       else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int))
    1.30 +         (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))))
    1.31     done)"
    1.32  
    1.33  instance ..
    1.34 @@ -229,7 +229,7 @@
    1.35  begin
    1.36  
    1.37  definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
    1.38 -  "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Eval.term_of (random n) split_seed"
    1.39 +  "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Code_Eval.term_of (random n) split_seed"
    1.40  
    1.41  instance ..
    1.42