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