# HG changeset patch
# User wenzelm
# Date 1415462141 -3600
# Node ID f6ecc0fb20662fe6639037a33bfae8ab67ec637a
# Parent  79684150ed6ad8dcc881cbeb6438f287f60a6a59
proper Envir.norm_type for result of Type.raw_unifys;

diff -r 79684150ed6a -r f6ecc0fb2066 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Sat Nov 08 16:42:04 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Sat Nov 08 16:55:41 2014 +0100
@@ -442,8 +442,8 @@
                 let
                   val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
                   val mgu = Type.raw_unifys unify_pairs Vartab.empty;
-                  val gen_tyargs' = map (Envir.subst_type mgu) gen_tyargs;
-                  val gen_seen' = map (Envir.subst_type mgu) gen_seen;
+                  val gen_tyargs' = map (Envir.norm_type mgu) gen_tyargs;
+                  val gen_seen' = map (Envir.norm_type mgu) gen_seen;
                 in
                   (rho, gen_tyargs', gen_seen', lthy)
                 end)