fixed typo in function name
authorblanchet
Thu, 09 Apr 2015 18:00:59 +0200
changeset 59988 c92afea6eb4b
parent 59987 fbe93138e540
child 59989 7b80ddb65e3e
fixed typo in function name
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;