1.1 --- a/src/Pure/logic.ML	Tue Jun 01 10:53:55 2010 +0200
     1.2 +++ b/src/Pure/logic.ML	Tue Jun 01 10:55:38 2010 +0200
     1.3 @@ -46,7 +46,8 @@
     1.4    val name_arity: string * sort list * class -> string
     1.5    val mk_arities: arity -> term list
     1.6    val dest_arity: term -> string * sort list * class
     1.7 -  val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
     1.8 +  val unconstrainT: sort list -> term -> 
     1.9 +    ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
    1.10    val protectC: term
    1.11    val protect: term -> term
    1.12    val unprotect: term -> term
    1.13 @@ -299,11 +300,15 @@
    1.14          map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
    1.15          constraints_map;
    1.16  
    1.17 +    val outer_constraints =
    1.18 +      maps (fn (T, S) => map (pair T) S)
    1.19 +        (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
    1.20 +
    1.21      val prop' =
    1.22        prop
    1.23        |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
    1.24        |> curry list_implies (map snd constraints);
    1.25 -  in ((atyp_map, constraints), prop') end;
    1.26 +  in ((atyp_map, constraints, outer_constraints), prop') end;
    1.27  
    1.28  
    1.29