# HG changeset patch
# User blanchet
# Date 1379093889 -7200
# Node ID f06b4f0723bb23af02a70e1c2d4b4272b0b23bd5
# Parent  9c3a80af72ff8dc674f8d3cfeb821a0f5dec023e
tuning

diff -r 9c3a80af72ff -r f06b4f0723bb src/HOL/BNF/Examples/Misc_Primrec.thy
--- a/src/HOL/BNF/Examples/Misc_Primrec.thy	Fri Sep 13 19:37:32 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Primrec.thy	Fri Sep 13 19:38:09 2013 +0200
@@ -71,7 +71,7 @@
   "mylist_of_forest (FCons t ts) = MyCons t (mylist_of_forest ts)"
 
 definition frev :: "'a forest \<Rightarrow> 'a forest" where
-  "frev = forest_of_mylist o myrev o mylist_of_forest"
+  "frev = forest_of_mylist \<circ> myrev \<circ> mylist_of_forest"
 
 primrec_new
   mirror_tree :: "'a tree \<Rightarrow> 'a tree" and
@@ -105,10 +105,10 @@
 
 primrec_new map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   "map_ftreeA f (FTLeaf x) = FTLeaf (f x)" |
-  "map_ftreeA f (FTNode g) = FTNode (map_ftreeA f o g)"
+  "map_ftreeA f (FTNode g) = FTNode (map_ftreeA f \<circ> g)"
 
 primrec_new map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where
   "map_ftreeB f (FTLeaf x) = FTLeaf (f x)" |
-  "map_ftreeB f (FTNode g) = FTNode (map_ftreeB f o g o the_inv f)"
+  "map_ftreeB f (FTNode g) = FTNode (map_ftreeB f \<circ> g \<circ> the_inv f)"
 
 end