--- a/Nominal/Ex/Classical.thy	Sat May 01 09:15:46 2010 +0100
+++ b/Nominal/Ex/Classical.thy	Sun May 02 14:06:26 2010 +0100
@@ -1,5 +1,5 @@
 theory Classical
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example from my Urban's PhD *)
@@ -8,7 +8,6 @@
   alpha_trm_raw is incorrectly defined, therefore the equivalence proof
   does not go through; below the correct definition is given
 *)
-ML {* val _ = cheat_equivp := true *}
 
 atom_decl name
 atom_decl coname
@@ -20,7 +19,7 @@
 |  AndL1 n::"name" t::"trm" "name"                              bind n in t
 |  AndL2 n::"name" t::"trm" "name"                              bind n in t
 |  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind n in t, bind c in t
+|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind n c in t
 
 
 thm trm.fv