compile
authorblanchet
Mon, 08 Sep 2014 14:03:13 +0200
changeset 58221 5451c61ee186
parent 58220 a2afad27a0b1
child 58222 0ea19fc3b957
compile
src/HOL/Library/Countable.thy
src/HOL/Library/bnf_lfp_countable.ML
--- 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
--- 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;