changeset 53309 | 42a99f732a40 |
parent 53304 | cfef783090eb |
child 53331 | 20440c789759 |
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Aug 30 12:09:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Aug 30 12:12:41 2013 +0200 @@ -355,7 +355,7 @@ end; (* These results are half broken. This is deliberate. We care only about those fields that are - used by "primrec_new", "primcorec", and "datatype_compat". *) + used by "primrec_new", "primcorec", and "datatype_new_compat". *) val fp_res = ({Ts = fpTs, bnfs = steal #bnfs,