src/HOL/Library/DAList.thy
changeset 51126 df86080de4cb
parent 49834 b27bbb021df1
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Library/DAList.thy	Thu Feb 14 17:58:28 2013 +0100
     1.2 +++ b/src/HOL/Library/DAList.thy	Thu Feb 14 15:27:10 2013 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4  
     1.5  fun (in term_syntax) random_aux_alist 
     1.6  where
     1.7 -  "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
     1.8 +  "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck_Random.collapse (Random.select_weight [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (%k. Quickcheck_Random.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
     1.9  
    1.10  instantiation alist :: (random, random) random
    1.11  begin