clarified signature -- some operations to support fully explicit proof terms;

--- a/src/Pure/logic.ML	Tue Oct 08 16:54:23 2019 +0200
+++ b/src/Pure/logic.ML	Wed Oct 09 21:59:56 2019 +0200
@@ -56,11 +56,13 @@
   val mk_arities: arity -> term list
   val mk_arity: string * sort list * class -> term
   val dest_arity: term -> string * sort list * class
+  val dummy_tfree: sort -> typ
   type unconstrain_context =
    {present_map: (typ * typ) list,
     constraints_map: (sort * typ) list,
     atyp_map: typ -> typ,
     map_atyps: typ -> typ,
+    map_atyps': typ -> typ,
     constraints: ((typ * class) * term) list,
     outer_constraints: (typ * class) list};
   val unconstrainT: sort list -> term -> unconstrain_context * term
@@ -170,6 +172,7 @@
   | dest_equals t = raise TERM ("dest_equals", [t]);
 
 
+
 (** implies **)
 
 val implies = Const ("Pure.imp", propT --> propT --> propT);
@@ -345,11 +348,14 @@
 
 (* internalized sort constraints *)
 
+fun dummy_tfree S = TFree ("'dummy", S);
+
 type unconstrain_context =
  {present_map: (typ * typ) list,
   constraints_map: (sort * typ) list,
   atyp_map: typ -> typ,
   map_atyps: typ -> typ,
+  map_atyps': typ -> typ,
   constraints: ((typ * class) * term) list,
   outer_constraints: (typ * class) list};
 
@@ -367,28 +373,41 @@
       map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
+    val present_map' = map (fn (T, T') => (Type.strip_sorts T', T)) present_map;
+    val constraints_map' = map (fn (S, T') => (Type.strip_sorts T', dummy_tfree S)) constraints_map;
+
     fun atyp_map T =
       (case AList.lookup (op =) present_map T of
         SOME U => U
       | NONE =>
           (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
             SOME U => U
-          | NONE => raise TYPE ("Dangling type variable", [T], [])));
+          | NONE => raise TYPE ("Dangling type variable ", [T], [prop])));
+
+    fun atyp_map' T =
+      (case AList.lookup (op =) present_map' T of
+        SOME U => U
+      | NONE =>
+          (case AList.lookup (op =) constraints_map' T of
+            SOME U => U
+          | NONE => raise TYPE ("Dangling type variable", [T], [prop])));
+
+    val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
+    val map_atyps' = Term.map_atyps atyp_map';
 
     val constraints =
       constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
         map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
 
     val outer_constraints =
-      maps (fn (T, S) => map (pair T) S)
-        (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
+      maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
 
-    val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
     val ucontext =
      {present_map = present_map,
       constraints_map = constraints_map,
       atyp_map = atyp_map,
       map_atyps = map_atyps,
+      map_atyps' = map_atyps',
       constraints = constraints,
       outer_constraints = outer_constraints};
     val prop' = prop

--- a/src/Pure/proofterm.ML	Tue Oct 08 16:54:23 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 09 21:59:56 2019 +0200
@@ -626,12 +626,12 @@
 fun del_conflicting_tvars envT T = Term_Subst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup envT ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvarsT T [])) T;
+        SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])) T;
 
 fun del_conflicting_vars env t = Term_Subst.instantiate
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
+        SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []),
    map_filter (fn (ixnT as (_, T)) =>
      (Envir.lookup env ixnT; NONE) handle TYPE _ =>
         SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
@@ -1055,7 +1055,7 @@
 fun strip_shyps_proof algebra present witnessed extra_sorts prf =
   let
     fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
-    val extra = map (fn S => (TFree ("'dummy", S), S)) extra_sorts;
+    val extra = map (`Logic.dummy_tfree) extra_sorts;
     val replacements = present @ extra @ witnessed;
     fun replace T =
       if exists (fn (T', _) => T' = T) present then raise Same.SAME