To be consistent with "induct", I renamed "fixing" to "arbitrary".
However I am not very fond of "arbitrary" - e.g. it clashes with
"arbitrary" of HOL. Both Gentzen (at least in the Szabo translation)
and Velleman (in How to prove it: a structured approach) use
"arbitrary".

Still, I wonder whether "generalising" is a good compromise?

--- a/src/HOL/Nominal/nominal_induct.ML	Thu Oct 12 15:50:43 2006 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Oct 12 22:03:33 2006 +0200
@@ -123,7 +123,7 @@
 local
 
 val avoidingN = "avoiding";
-val fixingN = "fixing";
+val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
 val ruleN = "rule";
 
 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;