Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper Envir.norm_type for result of Type.raw_unifys;
authorwenzelm
Sat, 08 Nov 2014 16:55:41 +0100
changeset 58948 f6ecc0fb2066
parent 58947 79684150ed6a
child 58949 e9559088ba29
proper Envir.norm_type for result of Type.raw_unifys;
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle