src/HOL/ex/Primrec.thy

   "\<forall>l. g l < ack (kg, list_add l) ==>
   fs \<in> lists(PRIMREC Int {f. \<exists>kf. \<forall>l. f l < ack(kf, list_add l)})
   ==> \<exists>k. \<forall>l. COMP g fs  l < ack(k, list_add l)"
   apply (unfold COMP_def)
   apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
-  apply (drule COMP_map_aux)
-  apply (meson ack_less_mono2 ack_nest_bound less_trans)
+    --{*Now, if meson tolerated map, we could finish with
+  @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans).*}
+  apply (erule COMP_map_aux [THEN exE])
+  apply (rule exI)
+  apply (rule allI)
+  apply (drule spec)+
+  apply (erule less_trans)
+  apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
   done
 
 
 text {* @{term PREC} case *}