# HG changeset patch
# User blanchet
# Date 1380664235 -7200
# Node ID 1878bab3e1c9f64c4abff224ef402b08f52397ed
# Parent  bd2e127389f2556e002475a05c25ef3548ecf50c
compile -- broken since 21dac9a60f0c

diff -r bd2e127389f2 -r 1878bab3e1c9 src/HOL/BNF/Examples/Misc_Primrec.thy
--- a/src/HOL/BNF/Examples/Misc_Primrec.thy	Tue Oct 01 23:36:02 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Primrec.thy	Tue Oct 01 23:50:35 2013 +0200
@@ -45,13 +45,13 @@
 primrec_new
   hf_size :: "hfset \<Rightarrow> nat"
 where
-  "hf_size (HFset X) = 1 + setsum id (fset (fmap hf_size X))"
+  "hf_size (HFset X) = 1 + setsum id (fset (fimage hf_size X))"
 
 primrec_new rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
   "rename_lam f (Var s) = Var (f s)" |
   "rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" |
   "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
-  "rename_lam f (Let SL l) = Let (fmap (map_pair f (rename_lam f)) SL) (rename_lam f l)"
+  "rename_lam f (Let SL l) = Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l)"
 
 primrec_new
   sum_i1 :: "('a\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and