changeset 56806 | f7d0520e7be2 |
parent 56805 | 8a87502c7da3 |
child 56858 | 0c3d0bc98abe |
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu May 01 14:05:29 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu May 01 14:07:27 2014 +0200 @@ -690,7 +690,7 @@ val sel_concls = sels ~~ ctr_args |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)) - handle UnequalLengths => + handle ListPair.UnequalLengths => primcorec_error_eqn "partially applied constructor in right-hand side" rhs; (*