src/Pure/logic.ML

   val name_arities: arity -> string list
   val name_arity: string * sort list * class -> string
   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
   val protectC: term
   val protect: term -> term

 
 fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u)
   | dest_equals t = raise TERM ("dest_equals", [t]);
 
 
+
 (** implies **)
 
 val implies = Const ("Pure.imp", propT --> propT --> propT);
 
 fun mk_implies (A, B) = implies $ A $ B;

   in (t, Ss, c) end;
 
 
 (* 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};
 
 fun unconstrainT shyps prop =
   let

     val present_map =
       map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
     val constraints_map =
       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);
-
-    val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
+      maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
+
     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
       |> Term.map_types map_atyps
       |> curry list_implies (map #2 constraints);