# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID aa50d903e0a7d043f3dc7a513ff44314203f1ff8
# Parent  75907f171d4ce5b0af13314b0d9c685965ce4909
adapted example

diff -r 75907f171d4c -r aa50d903e0a7 src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
@@ -147,7 +147,7 @@
 ML_file "Tools/BNF/bnf_comp_tactics.ML"
 ML_file "Tools/BNF/bnf_comp.ML"
 
-hide_const id_bnf_comp
-hide_fact id_bnf_comp_def type_definition_id_bnf_comp_UNIV
+hide_const (open) id_bnf_comp
+hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
 
 end
diff -r 75907f171d4c -r aa50d903e0a7 src/HOL/BNF_Examples/Stream.thy
--- a/src/HOL/BNF_Examples/Stream.thy	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream.thy	Mon Mar 03 12:48:20 2014 +0100
@@ -33,16 +33,16 @@
   assume "a \<in> set1_pre_stream (dtor_stream s)"
   then have "a = shd s"
     by (cases "dtor_stream s")
-      (auto simp: shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
-        Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+      (auto simp: BNF_Comp.id_bnf_comp_def shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
+        split: stream.splits)
   with Base show "P a s" by simp
 next
   fix a :: 'a and s' :: "'a stream"  and s :: "'a stream"
   assume "s' \<in> set2_pre_stream (dtor_stream s)" and prems: "a \<in> sset s'" "P a s'"
   then have "s' = stl s"
     by (cases "dtor_stream s")
-      (auto simp: stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
-        Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+      (auto simp: BNF_Comp.id_bnf_comp_def stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
+        split: stream.splits)
   with Step prems show "P a s" by simp
 qed