# HG changeset patch
# User blanchet
# Date 1410177793 -7200
# Node ID 5451c61ee186d2057cfc4a0e68254cedcfc2d643
# Parent  a2afad27a0b1ef0f3826a1c080f8c8921b8d7ee8
compile

diff -r a2afad27a0b1 -r 5451c61ee186 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Mon Sep 08 14:03:08 2014 +0200
+++ b/src/HOL/Library/Countable.thy	Mon Sep 08 14:03:13 2014 +0200
@@ -255,7 +255,7 @@
 text {* String literals *}
 
 instance String.literal :: countable
-  by (rule countable_classI [of "to_nat o String.explode"]) (auto simp add: explode_inject)
+  by (rule countable_classI [of "to_nat \<circ> String.explode"]) (auto simp add: explode_inject)
 
 text {* Functions *}
 
@@ -301,12 +301,12 @@
 begin
 
 lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
-  "\<rat> = range (of_rat o nat_to_rat_surj)"
+  "\<rat> = range (of_rat \<circ> nat_to_rat_surj)"
   using surj_nat_to_rat_surj
   by (auto simp: Rats_def image_def surj_def) (blast intro: arg_cong[where f = of_rat])
 
 lemma surj_of_rat_nat_to_rat_surj:
-  "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
+  "r \<in> \<rat> \<Longrightarrow> \<exists>n. r = of_rat (nat_to_rat_surj n)"
   by (simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
 
 end
diff -r a2afad27a0b1 -r 5451c61ee186 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Mon Sep 08 14:03:08 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Mon Sep 08 14:03:13 2014 +0200
@@ -88,8 +88,7 @@
       Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT);
 
     val nn = length ns;
-    val recs as rec1 :: _ =
-      map2 (fn fpT => mk_co_rec thy Least_FP fpT (replicate nn HOLogic.natT)) fpTs recs0;
+    val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0;
     val arg_Ts = binder_fun_types (fastype_of rec1);
     val arg_Tss = Library.unflat ctrss0 arg_Ts;