# HG changeset patch
# User haftmann
# Date 1245046568 -7200
# Node ID 138625ae4067f58d30a30b32fe07c56588f8c3f7
# Parent  8623244a50d568d3780657bfee64b6123b96eb97
where there is nothing, nothing can be hidden

diff -r 8623244a50d5 -r 138625ae4067 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Sun Jun 14 17:20:19 2009 +0200
+++ b/src/HOL/Random.thy	Mon Jun 15 08:16:08 2009 +0200
@@ -176,7 +176,7 @@
 
 hide (open) type seed
 hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
-  iterate range select pick select_weight select_default
+  iterate range select pick select_weight
 
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)