diff -r 01a13904aaa5 -r b69c8660de14 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Mon Oct 29 14:00:48 2012 +0000
+++ b/Nominal/nominal_mutual.ML	Thu Nov 29 21:59:38 2012 +0000
@@ -218,8 +218,11 @@
       | [cond] => ([Thm.assume cond], Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
       | _ => raise General.Fail "Too many conditions"
 
-    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt		   
+    val ([p], ctxt') = ctxt
+      |> fold Variable.declare_term args  
+      |> Variable.variant_fixes ["p"] 		   
     val p = Free (p, @{typ perm})
+
     val ss = HOL_basic_ss addsimps 
       @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @
       @{thms Projr.simps Projl.simps} @
@@ -350,6 +353,7 @@
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   let
     val result = inner_cont proof
+
     val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
       termination, domintros, eqvts=[eqvt],...} = result