# HG changeset patch
# User haftmann
# Date 1166426492 -3600
# Node ID 96a601bc59d88b7790b79a7e91ee068c71d520bd
# Parent  5df10a17644e319be77a3092b7d6ea770ea70b3d
dropped debug cmd

diff -r 5df10a17644e -r 96a601bc59d8 src/HOL/ex/CodeRandom.thy
--- 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