# HG changeset patch
# User immler
# Date 1352992072 -3600
# Node ID 01203193dfa07c8f16ac8bc9ad005b9623adee17
# Parent  1badf63e5d977cc45ca96c1883090a7d90ffc958
hide constants of auxiliary type finmap

diff -r 1badf63e5d97 -r 01203193dfa0 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Thu Nov 15 15:50:01 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Thu Nov 15 16:07:52 2012 +0100
@@ -620,6 +620,17 @@
 
 end
 
+hide_const (open) PiF
+hide_const (open) Pi\<^isub>F
+hide_const (open) Pi'
+hide_const (open) Abs_finmap
+hide_const (open) Rep_finmap
+hide_const (open) finmap_of
+hide_const (open) finmapset
+hide_const (open) proj
+hide_const (open) domain
+hide_const (open) enum_basis_finmap
+
 sublocale polish_projective \<subseteq> P!: prob_space "(PiB I P)"
 proof
   show "emeasure (PiB I P) (space (PiB I P)) = 1"