diff -r a8ebcb368a15 -r e5fa8de0e4bd Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Thu Jan 06 23:06:45 2011 +0000
+++ b/Nominal/nominal_eqvt.ML	Fri Jan 07 02:30:00 2011 +0000
@@ -10,7 +10,8 @@
   val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
   val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
   
-  val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
+  val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
+  val equivariance: string -> Proof.context -> (thm list * local_theory)
   val equivariance_cmd: string -> Proof.context -> local_theory
 end
 
@@ -60,7 +61,7 @@
   let
     val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros
   in
-    EVERY' (rtac induct :: cases)
+    EVERY' ((DETERM o rtac induct) :: cases)
   end
 
 
@@ -85,7 +86,10 @@
     (thm', ctxt')
   end
 
-fun equivariance note_flag pred_trms raw_induct intrs ctxt = 
+fun get_name (Const (a, _)) = a
+  | get_name (Free  (a, _)) = a
+
+fun raw_equivariance note_flag pred_trms raw_induct intrs ctxt = 
   let
     val is_already_eqvt = 
       filter (is_eqvt ctxt) pred_trms
@@ -93,7 +97,7 @@
     val _ = if null is_already_eqvt then ()
       else error ("Already equivariant: " ^ commas is_already_eqvt)
 
-    val pred_names = map (fst o dest_Const) pred_trms
+    val pred_names = map get_name pred_trms
     val raw_induct' = atomize_induct ctxt raw_induct
     val intrs' = map atomize_intr intrs
   
@@ -121,13 +125,22 @@
     else (thms, ctxt) 
   end
 
+fun equivariance pred_name ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val (_, {preds, raw_induct, intrs, ...}) =
+      Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
+  in
+    raw_equivariance false preds raw_induct intrs ctxt 
+  end
+
 fun equivariance_cmd pred_name ctxt =
   let
     val thy = ProofContext.theory_of ctxt
     val (_, {preds, raw_induct, intrs, ...}) =
       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
   in
-    equivariance true preds raw_induct intrs ctxt |> snd
+    raw_equivariance true preds raw_induct intrs ctxt |> snd
   end
 
 local structure P = Parse and K = Keyword in