diff -r a8724924a62e -r 13ab4f0a0b0e Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Mar 26 16:41:31 2013 +0100
+++ b/Nominal/Nominal2.thy	Wed Mar 27 16:08:30 2013 +0100
@@ -281,7 +281,7 @@
     let
       val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result
     in
-      Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros lthy5
+      Nominal_Eqvt.raw_equivariance lthy5 (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros
     end
 
   val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt
@@ -445,7 +445,7 @@
     |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
     |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
 
-  (* filters the theormes that are of the form "qfv = supp" *)
+  (* filters the theorems that are of the form "qfv = supp" *)
   fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs
   | is_qfv_thm _ = false
 
@@ -742,8 +742,4 @@
     (main_parser >> nominal_datatype2_cmd)
 *}
 
-
 end
-
-
-