--- a/Nominal/NewParser.thy	Wed Jun 02 11:37:51 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Jun 03 11:48:44 2010 +0200
@@ -399,7 +399,8 @@
 
   val fv_eqvt = 
     if get_STEPS lthy > 7
-    then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp
+    then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) 
+       (Local_Theory.restore lthy_tmp)
     else raise TEST lthy4
  
   val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
@@ -409,10 +410,6 @@
     then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp'
     else raise TEST lthy4
 
-  val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt))
-  val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt))
-  val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt))
-
   val _ = 
     if get_STEPS lthy > 9
     then true else raise TEST lthy4