--- 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;