--- 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
changeset 21876	96a601bc59d8
parent 21545	54cc492d80a9
child 21912	ff45788e7bf9