--- a/Nominal-General/nominal_eqvt.ML	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Wed May 05 10:24:54 2010 +0100
@@ -75,9 +75,9 @@
 *)
 fun transform_prem ctxt names thm =
 let
-  fun split_conj names (Const ("op &", _) $ p $ q) = 
-      (case head_of p of
-         Const (name, _) => if name mem names then SOME q else NONE
+  fun split_conj names (Const ("op &", _) $ f1 $ f2) = 
+      (case head_of f1 of
+         Const (name, _) => if name mem names then SOME f2 else NONE
        | _ => NONE)
   | split_conj _ _ = NONE;
 in
@@ -102,6 +102,7 @@
   SUBPROOF (fn {prems, context as ctxt, ...} =>
     let
       val prems' = map (transform_prem ctxt pred_names) prems
+
       val tac1 = resolve_tac prems'
       val tac2 = EVERY' [ rtac pi_intro_rule, 
             eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]