# HG changeset patch
# User urbanc
# Date 1160683413 -7200
# Node ID 714a08286899b7474af075a5a5e972985f876241
# Parent  4b500d78cb4f24207615ec9b4a3fb08c87f2d730
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?

diff -r 4b500d78cb4f -r 714a08286899 src/HOL/Nominal/nominal_induct.ML
--- 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;