src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
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;
 
 (*