tuned signature;

--- a/src/Pure/logic.ML	Mon Jul 29 11:09:37 2019 +0200
+++ b/src/Pure/logic.ML	Mon Jul 29 11:21:41 2019 +0200
@@ -60,6 +60,7 @@
    {present_map: (typ * typ) list,
     extra_map: (sort * typ) list,
     atyp_map: typ -> typ,
+    map_atyps: typ -> typ,
     constraints: ((typ * class) * term) list,
     outer_constraints: (typ * class) list};
   val unconstrainT: sort list -> term -> unconstrain_context * term
@@ -348,6 +349,7 @@
  {present_map: (typ * typ) list,
   extra_map: (sort * typ) list,
   atyp_map: typ -> typ,
+  map_atyps: typ -> typ,
   constraints: ((typ * class) * term) list,
   outer_constraints: (typ * class) list};
 
@@ -382,16 +384,18 @@
       maps (fn (T, S) => map (pair T) S)
         (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
 
-    val context =
+    val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
+    val ucontext =
      {present_map = present_map,
       extra_map = extra_map,
       atyp_map = atyp_map,
+      map_atyps = map_atyps,
       constraints = constraints,
       outer_constraints = outer_constraints};
     val prop' = prop
-      |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
-      |> curry list_implies (map snd constraints);
-  in (context, prop') end;
+      |> Term.map_types map_atyps
+      |> curry list_implies (map #2 constraints);
+  in (ucontext, prop') end;
 
 
 

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