# HG changeset patch
# User blanchet
# Date 1428595259 -7200
# Node ID c92afea6eb4ba773a38276e7be507515cdbd7eb2
# Parent  fbe93138e54037e8613d0e3f6c27584c40f3ecc0
fixed typo in function name

diff -r fbe93138e540 -r c92afea6eb4b src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Apr 09 18:00:59 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Apr 09 18:00:59 2015 +0200
@@ -54,7 +54,7 @@
 
 fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero;
 
-fun mk_pointfull ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong);
+fun mk_pointful ctxt thm = unfold_thms ctxt [o_apply] (thm RS fun_cong);
 
 fun mk_unabs_def_unused_0 n =
   funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
@@ -235,7 +235,7 @@
         (Spec_Rules.retrieve lthy0 @{const size ('a)}
          |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
 
-      val nested_size_maps = map (mk_pointfull lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
+      val nested_size_maps = map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
       val all_inj_maps =
         @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
         |> distinct Thm.eq_thm_prop;