tuned signature;

--- a/src/HOL/Nominal/nominal_induct.ML	Wed Oct 12 21:39:33 2011 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Oct 12 22:21:38 2011 +0200
@@ -114,10 +114,9 @@
               Method.insert_tac (more_facts @ adefs) THEN'
                 (if simp then
                    Induct.rotate_tac k (length adefs) THEN'
-                   Induct.fix_tac defs_ctxt k
-                     (List.partition (member op = frees) xs |> op @)
+                   Induct.arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
                  else
-                   Induct.fix_tac defs_ctxt k xs)
+                   Induct.arbitrary_tac defs_ctxt k xs)
             end)
           THEN' Induct.inner_atomize_tac) j))
         THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>

--- a/src/Tools/induct.ML	Wed Oct 12 21:39:33 2011 +0200
+++ b/src/Tools/induct.ML	Wed Oct 12 22:21:38 2011 +0200
@@ -56,7 +56,7 @@
   val predN: string
   val setN: string
   (*proof methods*)
-  val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
+  val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
   val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
     (term option list * thm list) * Proof.context
   val atomize_term: theory -> term -> term
@@ -637,7 +637,7 @@
   | special_rename_params _ _ ths = ths;
 
 
-(* fix_tac *)
+(* arbitrary_tac *)
 
 local
 
@@ -685,8 +685,8 @@
 
 in
 
-fun fix_tac _ _ [] = K all_tac
-  | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
+fun arbitrary_tac _ _ [] = K all_tac
+  | arbitrary_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
      (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
       (miniscope_tac (goal_params n goal) ctxt)) i);
 
@@ -784,9 +784,9 @@
               Method.insert_tac (more_facts @ adefs) THEN'
                 (if simp then
                    rotate_tac k (length adefs) THEN'
-                   fix_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
+                   arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
                  else
-                   fix_tac defs_ctxt k xs)
+                   arbitrary_tac defs_ctxt k xs)
              end)
           THEN' inner_atomize_tac) j))
         THEN' atomize_tac) i st |> Seq.maps (fn st' =>