# HG changeset patch
# User haftmann
# Date 1266587220 -3600
# Node ID 07a56610c00bd49e2d1d54a8fb552f9175db829a
# Parent  3fd8c3edf6398ccd710c68fd65090cc9c50bc300
hide fact range_def

diff -r 3fd8c3edf639 -r 07a56610c00b src/HOL/Random.thy
--- a/src/HOL/Random.thy	Fri Feb 19 14:47:00 2010 +0100
+++ b/src/HOL/Random.thy	Fri Feb 19 14:47:00 2010 +0100
@@ -168,6 +168,7 @@
 hide (open) type seed
 hide (open) const inc_shift minus_shift log "next" split_seed
   iterate range select pick select_weight
+hide (open) fact range_def
 
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)