diff -r 082d9fd28f89 -r ebf253d80670 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri Jul 30 00:40:32 2010 +0100
@@ -258,11 +258,11 @@
 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}
 
 fun subproof_tac const_names simps = 
-  Subgoal.FOCUS (fn {prems, context, ...} => 
+  SUBPROOF (fn {prems, context, ...} => 
     HEADGOAL 
       (simp_tac (HOL_basic_ss addsimps simps)
        THEN' Nominal_Permeq.eqvt_tac context [] const_names
-       THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems))))
+       THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
 
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
   HEADGOAL