src/Pure/logic.ML
changeset 36768 46be86127972
parent 36767 d0095729e1f1
child 37230 7b548f137276
     1.1 --- a/src/Pure/logic.ML	Sun May 09 18:09:30 2010 +0200
     1.2 +++ b/src/Pure/logic.ML	Sun May 09 19:15:21 2010 +0200
     1.3 @@ -46,7 +46,7 @@
     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 unconstrain_allTs: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
     1.8 +  val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
     1.9    val protectC: term
    1.10    val protect: term -> term
    1.11    val unprotect: term -> term
    1.12 @@ -272,7 +272,7 @@
    1.13  
    1.14  (* internalized sort constraints *)
    1.15  
    1.16 -fun unconstrain_allTs shyps prop =
    1.17 +fun unconstrainT shyps prop =
    1.18    let
    1.19      val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
    1.20      val extra = fold (Sorts.remove_sort o #2) present shyps;