tuned signature;

--- a/src/HOL/Nominal/nominal_induct.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -72,7 +72,7 @@
         val ys =
           if p < n then []
           else map (tune o #1) (take (p - n) ps) @ xs;
-      in Logic.list_rename_params (ys, prem) end;
+      in Logic.list_rename_params ys prem end;
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;

--- a/src/Pure/Isar/obtain.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -138,11 +138,11 @@
 
     val that_name = if name = "" then thatN else name;
     val that_prop =
-      Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))
-      |> Library.curry Logic.list_rename_params xs;
+      Logic.list_rename_params xs
+        (Term.list_all_free (parms, Logic.list_implies (asm_props, thesis)));
     val obtain_prop =
-      Logic.list_rename_params ([Auto_Bind.thesisN],
-        Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
+      Logic.list_rename_params [Auto_Bind.thesisN]
+        (Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
 
     fun after_qed _ =
       Proof.local_qed (NONE, false)

--- a/src/Pure/Isar/rule_cases.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -403,7 +403,7 @@
     fun rename prem =
       let val xs =
         map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
-      in Logic.list_rename_params (xs, prem) end;
+      in Logic.list_rename_params xs prem end;
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;

--- a/src/Pure/logic.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/Pure/logic.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -46,7 +46,7 @@
   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
@@ -68,8 +68,8 @@
   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
@@ -453,11 +453,11 @@
     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;
 
 
 

--- a/src/Pure/thm.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/Pure/thm.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -1494,7 +1494,7 @@
       if short < 0 then error "More names than abstractions!"
       else Name.variant_list cs (take short iparams) @ cs;
     val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
-    val newBi = Logic.list_rename_params (newnames, Bi);
+    val newBi = Logic.list_rename_params newnames Bi;
   in
     (case duplicates (op =) cs of
       a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)

--- a/src/Tools/induct.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/Tools/induct.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -627,7 +627,7 @@
             val xs' =
               (case filter (fn x' => x' = x) xs of
                 [] => xs | [_] => xs | _ => index 1 xs);
-          in Logic.list_rename_params (xs', A) end;
+          in Logic.list_rename_params xs' A end;
         fun rename_prop p =
           let val (As, C) = Logic.strip_horn p
           in Logic.list_implies (map rename_asm As, C) end;