diff -r 39c387e690aa -r 301b74fcd614 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Mar 14 15:41:54 2012 +0000 +++ b/Nominal/Ex/Lambda.thy Sat Mar 17 05:13:59 2012 +0000 @@ -887,7 +887,7 @@ text {* tests of functions containing if and case *} -(*consts P :: "lam \ bool" +consts P :: "lam \ bool" nominal_primrec A :: "lam => lam" @@ -924,7 +924,7 @@ apply(perm_simp) apply(rule allI) apply(rule refl) -oops*) +oops end