1.1 --- a/src/HOL/ex/Random.thy	Sun May 06 21:49:44 2007 +0200
     1.2 +++ b/src/HOL/ex/Random.thy	Sun May 06 21:50:17 2007 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  where
     1.5    pick_undef: "pick [] n = undefined"
     1.6    | pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
     1.7 -lemmas [code nofunc] = pick_undef
     1.8 +lemmas [code func del] = pick_undef
     1.9  
    1.10  typedecl randseed
    1.11  
    1.12 @@ -180,7 +180,4 @@
    1.13  code_const run_random
    1.14    (SML "case _ (Random.seed ()) of (x, '_) => x")
    1.15  
    1.16 -code_gen select select_weight
    1.17 -  (SML #)
    1.18 -
    1.19  end