diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/BNF/Examples/TreeFsetI.thy --- a/src/HOL/BNF/Examples/TreeFsetI.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFsetI.thy Tue Aug 13 15:59:22 2013 +0200 @@ -12,7 +12,7 @@ imports "../BNF" begin -hide_fact (open) Quotient_Product.prod_rel_def +hide_fact (open) Lifting_Product.prod_rel_def codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")