--- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 22 07:18:36 2016 +0100
@@ -779,8 +779,8 @@
(case (absT, absU) of
(Type (C, Ts), Type (C', Us)) =>
if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT
- else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
- | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
+ else raise Term.TYPE ("mk_repT", [absT, repT, absU], [])
+ | _ => raise Term.TYPE ("mk_repT", [absT, repT, absU], []));
fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf}, _)) =
Const (@{const_name id_bnf}, absU --> absU)