# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1354226378 0
# Node ID b69c8660de1495940b0e287bf51a0f265051971d
# Parent  01a13904aaa51bb300b17208507a5902076b5e4e
fixed problem with not fresh enough permutation name in nominal_primrec

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
 
diff -r 01a13904aaa5 -r b69c8660de14 README
--- a/README	Mon Oct 29 14:00:48 2012 +0000
+++ b/README	Thu Nov 29 21:59:38 2012 +0000
@@ -1,6 +1,11 @@
 This repository contain a new implementation of
 Nominal Isabelle.
 
+Compilation of Tests
+====================
+
+isabelle build -d . -g Tests
+
 
 Subdirectories:
 ===============