src/Pure/logic.ML
changeset 45328 e5b33eecbf6e
parent 43329 84472e198515
child 45344 e209da839ff4
     1.1 --- a/src/Pure/logic.ML	Thu Nov 03 22:23:41 2011 +0100
     1.2 +++ b/src/Pure/logic.ML	Thu Nov 03 22:51:37 2011 +0100
     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 unconstrainT: sort 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 @@ -68,8 +68,8 @@
    1.13    val strip_params: term -> (string * typ) list
    1.14    val has_meta_prems: term -> bool
    1.15    val flatten_params: int -> term -> term
    1.16 -  val list_rename_params: string list * term -> term
    1.17 -  val assum_pairs: int * term -> (term*term)list
    1.18 +  val list_rename_params: string list -> term -> term
    1.19 +  val assum_pairs: int * term -> (term * term) list
    1.20    val assum_problems: int * term -> (term -> term) * term list * term
    1.21    val varifyT_global: typ -> typ
    1.22    val unvarifyT_global: typ -> typ
    1.23 @@ -453,11 +453,11 @@
    1.24      end;
    1.25  
    1.26  (*Makes parameters in a goal have the names supplied by the list cs.*)
    1.27 -fun list_rename_params (cs, Const("==>", _) $ A $ B) =
    1.28 -      implies $ A $ list_rename_params (cs, B)
    1.29 -  | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
    1.30 -      a $ Abs(c, T, list_rename_params (cs, t))
    1.31 -  | list_rename_params (cs, B) = B;
    1.32 +fun list_rename_params cs (Const ("==>", _) $ A $ B) =
    1.33 +      implies $ A $ list_rename_params cs B
    1.34 +  | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
    1.35 +      a $ Abs (c, T, list_rename_params cs t)
    1.36 +  | list_rename_params cs B = B;
    1.37  
    1.38  
    1.39