--- a/src/HOL/BNF/More_BNFs.thy Fri Jul 05 18:10:07 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Sun Jul 07 10:24:00 2013 +0200
@@ -129,7 +129,7 @@
apply (rule ordLeq_transitive)
apply (rule card_of_list_in)
apply (rule ordLeq_transitive)
- apply (erule card_of_Pfunc_Pow_Func)
+ apply (erule card_of_Pfunc_Pow_Func_option)
apply (rule ordIso_ordLeq_trans)
apply (rule Times_cprod)
apply (rule cprod_cinfinite_bound)
@@ -145,6 +145,8 @@
apply (rule Card_order_ctwo)
apply (rule natLeq_Card_order)
apply (rule ordIso_ordLeq_trans)
+ apply (rule card_of_Func_option_Func)
+ apply (rule ordIso_ordLeq_trans)
apply (rule card_of_Func)
apply (rule ordIso_ordLeq_trans)
apply (rule cexp_cong2)