src/Pure/logic.ML

--- a/src/Pure/logic.ML	Tue Jun 01 10:53:55 2010 +0200
+++ b/src/Pure/logic.ML	Tue Jun 01 10:55:38 2010 +0200
@@ -46,7 +46,8 @@
   val name_arity: string * sort list * class -> string
   val mk_arities: arity -> term list
   val dest_arity: term -> string * sort list * class
-  val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
+  val unconstrainT: sort list -> term -> 
+    ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -299,11 +300,15 @@
         map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
         constraints_map;
 
+    val outer_constraints =
+      maps (fn (T, S) => map (pair T) S)
+        (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
+
     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, constraints), prop') end;
+  in ((atyp_map, constraints, outer_constraints), prop') end;