changeset 55531 | 601ca8efa000 |
parent 55530 | 3dfb724db099 |
child 55539 | 0819931d652d |
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 13:31:42 2014 +0100 @@ -355,7 +355,7 @@ end; (* These results are half broken. This is deliberate. We care only about those fields that are - used by "primrec", "primcorecursive", and "datatype_new_compat". *) + used by "primrec", "primcorecursive", and "datatype_compat". *) val fp_res = ({Ts = fpTs, bnfs = steal #bnfs,