--- a/src/HOL/ex/CodeRandom.thy Mon Dec 18 08:21:31 2006 +0100 +++ b/src/HOL/ex/CodeRandom.thy Mon Dec 18 08:21:32 2006 +0100 @@ -189,6 +189,4 @@ code_gen select select_weight (SML #) -code_gen (SML -) - end \ No newline at end of file