# HG changeset patch
# User Christian Sternagel
# Date 1346301855 -32400
# Node ID 5eddc9aaebf1a5cba794d34e595c917c5f998399
# Parent  0da7116b1b23474cca8596434776854d0f15ec2f
hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI

diff -r 0da7116b1b23 -r 5eddc9aaebf1 src/HOL/Codatatype/Examples/TreeFI.thy
--- a/src/HOL/Codatatype/Examples/TreeFI.thy	Thu Aug 30 13:39:43 2012 +0900
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy	Thu Aug 30 13:44:15 2012 +0900
@@ -12,6 +12,8 @@
 imports ListF
 begin
 
+hide_const (open) Sublist.sub
+
 bnf_codata treeFI: 'tree = "'a \<times> 'tree listF"
 
 lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs"
diff -r 0da7116b1b23 -r 5eddc9aaebf1 src/HOL/Codatatype/Examples/TreeFsetI.thy
--- 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)"