--- a/Nominal-General/nominal_eqvt.ML	Thu Apr 15 21:56:03 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Fri Apr 16 10:18:16 2010 +0200
@@ -146,7 +146,7 @@
   val params_no = length (Inductive.params_of raw_induct)
   val (([raw_concl], [raw_pi]), ctxt') = ctxt 
          |> Variable.import_terms false [concl_of raw_induct] 
-         ||>> Variable.variant_fixes ["pi"]
+         ||>> Variable.variant_fixes ["p"]
   val pi = Free (raw_pi, @{typ perm})
   val preds = map (fst o HOLogic.dest_imp)
     (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));