--- a/Nominal/Ex/ExPS7.thy Sun Aug 29 12:17:25 2010 +0800 +++ b/Nominal/Ex/ExPS7.thy Sun Aug 29 13:36:03 2010 +0800 @@ -1,6 +1,5 @@ - theory ExPS7 -imports "../NewParser" +imports "../Nominal2" begin (* example 7 from Peter Sewell's bestiary *)