src/HOL/Codatatype/Examples/TreeFsetI.thy
changeset 49092 5eddc9aaebf1
parent 48980 debfa361f648
child 49094 7b6beb7e99c1
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy	Thu Aug 30 13:39:43 2012 +0900
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy	Thu Aug 30 13:44:15 2012 +0900
@@ -12,6 +12,8 @@
 imports "../Codatatype"
 begin
 
+hide_const (open) Sublist.sub
+
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"