src/Pure/logic.ML

   val dest_classrel: term -> class * class
   val name_arities: arity -> string list
   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 -> 
+  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
   val mk_term: term -> term

   val strip_assums_hyp: term -> term list
   val strip_assums_concl: term -> term
   val strip_params: term -> (string * typ) list
   val has_meta_prems: term -> bool
   val flatten_params: int -> term -> term
-  val list_rename_params: string list * term -> term
-  val assum_pairs: int * term -> (term*term)list
+  val list_rename_params: string list -> term -> term
+  val assum_pairs: int * term -> (term * term) list
   val assum_problems: int * term -> (term -> term) * term list * term
   val varifyT_global: typ -> typ
   val unvarifyT_global: typ -> typ
   val varify_global: term -> term
   val unvarify_global: term -> term

                                  map #2 params)
     in  list_all (vars, remove_params (length vars) n A)
     end;
 
 (*Makes parameters in a goal have the names supplied by the list cs.*)
-fun list_rename_params (cs, Const("==>", _) $ A $ B) =
-      implies $ A $ list_rename_params (cs, B)
-  | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
-      a $ Abs(c, T, list_rename_params (cs, t))
-  | list_rename_params (cs, B) = B;
+fun list_rename_params cs (Const ("==>", _) $ A $ B) =
+      implies $ A $ list_rename_params cs B
+  | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
+      a $ Abs (c, T, list_rename_params cs t)
+  | list_rename_params cs B = B;
 
 
 
 (*** Treatment of "assume", "erule", etc. ***)