1.1 --- a/src/HOL/Library/Fin_Fun.thy	Wed Sep 23 13:42:53 2009 +0200
     1.2 +++ b/src/HOL/Library/Fin_Fun.thy	Wed Sep 23 14:00:12 2009 +0200
     1.3 @@ -311,17 +311,17 @@
     1.4  notation scomp (infixl "o\<rightarrow>" 60)
     1.5  
     1.6  definition (in term_syntax) valtermify_finfun_const ::
     1.7 -  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
     1.8 -  "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
     1.9 +  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    1.10 +  "valtermify_finfun_const y = Code_Evaluation.valtermify finfun_const {\<cdot>} y"
    1.11  
    1.12  definition (in term_syntax) valtermify_finfun_update_code ::
    1.13 -  "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
    1.14 -  "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
    1.15 +  "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    1.16 +  "valtermify_finfun_update_code x y f = Code_Evaluation.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
    1.17  
    1.18  instantiation finfun :: (random, random) random
    1.19  begin
    1.20  
    1.21 -primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
    1.22 +primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
    1.23      "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
    1.24         [(1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
    1.25    | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight