# HG changeset patch
# User blanchet
# Date 1384440006 -3600
# Node ID e9ff6a25aaa6d2a666b248076d34df3305229722
# Parent  be1bc181bcde93b6c75cb6416dac322dc7520c11
renamed thm

diff -r be1bc181bcde -r e9ff6a25aaa6 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Thu Nov 14 13:03:09 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Thu Nov 14 15:40:06 2013 +0100
@@ -206,7 +206,7 @@
   by (transfer, clarsimp, metis fst_conv)
 qed
 
-lemma wpull_fmap:
+lemma wpull_fimage:
   assumes "wpull A B1 B2 f1 f2 p1 p2"
   shows "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
               (fimage f1) (fimage f2) (fimage p1) (fimage p2)"
@@ -245,7 +245,7 @@
       apply (rule natLeq_card_order)
      apply (rule natLeq_cinfinite)
     apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
-  apply (erule wpull_fmap)
+  apply (erule wpull_fimage)
  apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
 apply transfer apply simp
 done