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