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 unconstrainT: sort list -> term ->
-   {atyp_map: typ -> typ,
+  type unconstrain_context =
+   {present_map: (typ * typ) list,
+    extra_map: (sort * typ) list,
+    atyp_map: typ -> typ,
     constraints: ((typ * class) * term) list,
-    outer_constraints: (typ * class) list,
-    prop: term}
+    outer_constraints: (typ * class) list};
+  val unconstrainT: sort list -> term -> unconstrain_context * term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
   val mk_term: term -> term
   val dest_term: term -> term

   in (t, Ss, c) end;
 
 
 (* internalized sort constraints *)
 
+type unconstrain_context =
+ {present_map: (typ * typ) list,
+  extra_map: (sort * typ) list,
+  atyp_map: typ -> typ,
+  constraints: ((typ * class) * term) list,
+  outer_constraints: (typ * class) list};
+
 fun unconstrainT shyps prop =
   let
     val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
     val extra = fold (Sorts.remove_sort o #2) present shyps;
 
     val n = length present;
     val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
 
     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 @
+    val extra_map =
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
     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
+          (case AList.lookup (op =) extra_map (Type.sort_of_atyp T) of
             SOME U => U
           | NONE => raise TYPE ("Dangling type variable", [T], [])));
 
+    val constraints_map =
+      map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ extra_map;
     val constraints =
-      maps (fn (_, T as TVar (ai, S)) =>
-        map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
-        constraints_map;
+      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 prop' =
-      prop
+    val context =
+     {present_map = present_map,
+      extra_map = extra_map,
+      atyp_map = atyp_map,
+      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
-   {atyp_map = atyp_map,
-    constraints = constraints,
-    outer_constraints = outer_constraints,
-    prop = prop'}
-  end;
+  in (context, prop') end;
 
 
 
 (** protected propositions and embedded terms **)