proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);

--- 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