src/HOL/ex/CodeRandom.thy
changeset 21125 9b7d35ca1eef
parent 21113 5b76e541cc0a
child 21192 5fe5cd5fede7
--- a/src/HOL/ex/CodeRandom.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -182,6 +182,6 @@
   (SML "case _ (Random.seed ()) of (x, '_) => x")
 
 code_gen select select_weight
-  (SML -)
+  (SML *)
 
 end
\ No newline at end of file