src/Pure/proofterm.ML

 
     val prop = Logic.list_implies (hyps, concl);
     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;
     val body0 =
       Future.value