src/HOL/Tools/BNF/bnf_lfp_size.ML

         all_inj_maps @ nested_size_maps) lthy2)
       |> fold_thms lthy2 size_defs_unused_0;
     fun derive_overloaded_size_simp size_def' simp0 =
       (trans OF [size_def', simp0])
       |> unfold_thms lthy2 @{thms add_0_left add_0_right}
-      |> fold_thms lthy2 overloaded_size_defs';
+      |> fold_thms lthy2 overloaded_size_defs;
 
     val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
     val size_simps = flat size_simpss;
     val overloaded_size_simpss =
       map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;