diff -r 251f1fb44ccd -r fdbb0c2e0162 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 29 11:09:37 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 29 11:21:41 2019 +0200
@@ -1710,9 +1710,7 @@
     val args = prop_args prop;
 
     val (ucontext, prop1) = Logic.unconstrainT shyps prop;
-    val args1 =
-      (map o Option.map o Term.map_types o Term.map_atyps)
-        (Type.strip_sorts o #atyp_map ucontext) args;
+    val args1 = (map o Option.map o Term.map_types) (#map_atyps ucontext) args;
     val argsP = map OfClass (#outer_constraints ucontext) @ map Hyp hyps;
 
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;