# HG changeset patch
# User wenzelm
# Date 1415460924 -3600
# Node ID 3bf80312508e95b961e9864a3102ec0267a43dc9
# Parent  cfb254e6c261c13e513224c08f973bd92a6e5250
proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);

diff -r cfb254e6c261 -r 3bf80312508e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Nov 08 15:45:00 2014 +0100
+++ b/src/Pure/thm.ML	Sat Nov 08 16:35:24 2014 +0100
@@ -1545,7 +1545,7 @@
 fun norm_term_skip env 0 t = Envir.norm_term env t
   | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) =
       let
-        val T' = Envir.subst_type (Envir.type_env env) T
+        val T' = Envir.norm_type (Envir.type_env env) T
         (*Must instantiate types of parameters because they are flattened;
           this could be a NEW parameter*)
       in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end