# HG changeset patch
# User haftmann
# Date 1253034995 -7200
# Node ID a382876d3290519aac943bb3482ed43d8421f55c
# Parent  44ac2e398411499bd1db218ce27910af2c4f75fc
hide new constants

diff -r 44ac2e398411 -r a382876d3290 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Sep 15 15:41:30 2009 +0200
+++ b/src/HOL/Predicate.thy	Tue Sep 15 19:16:35 2009 +0200
@@ -874,7 +874,7 @@
   bind (infixl "\<guillemotright>=" 70)
 
 hide (open) type pred seq
-hide (open) const Pred eval single bind if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
+hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
 
 end