--- a/Nominal/nominal_eqvt.ML	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/nominal_eqvt.ML	Thu Jun 16 20:07:03 2011 +0100
@@ -8,8 +8,7 @@
 
 signature NOMINAL_EQVT =
 sig
-  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 raw_equivariance: term list -> thm -> thm list -> Proof.context -> thm list
   val equivariance_cmd: string -> Proof.context -> local_theory
 end
 
@@ -75,20 +74,10 @@
 
 (* stores thm under name.eqvt and adds [eqvt]-attribute *)
 
-fun note_named_thm (name, thm) ctxt = 
-  let
-    val thm_name = Binding.qualified_name 
-      (Long_Name.qualify (Long_Name.base_name name) "eqvt")
-    val attr = Attrib.internal (K eqvt_add)
-    val ((_, [thm']), ctxt') =  Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
-  in
-    (thm', ctxt')
-  end
-
 fun get_name (Const (a, _)) = a
   | get_name (Free  (a, _)) = a
 
-fun raw_equivariance note_flag pred_trms raw_induct intrs ctxt = 
+fun raw_equivariance pred_trms raw_induct intrs ctxt = 
   let
     val is_already_eqvt = 
       filter (is_eqvt ctxt) pred_trms
@@ -110,36 +99,34 @@
       (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));
   
     val goal = HOLogic.mk_Trueprop 
-      (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds))
-  
-    val thms = Goal.prove ctxt' [] [] goal 
+      (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) 
+  in 
+    Goal.prove ctxt' [] [] goal 
       (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1)
       |> Datatype_Aux.split_conj_thm 
       |> ProofContext.export ctxt' ctxt
       |> map (fn th => th RS mp)
       |> map zero_var_indexes
-  in
-    if note_flag
-    then fold_map note_named_thm (pred_names ~~ thms) ctxt 
-    else (thms, ctxt) 
   end
 
-fun equivariance pred_name ctxt =
+fun note_named_thm (name, thm) ctxt = 
   let
-    val thy = ProofContext.theory_of ctxt
-    val (_, {preds, raw_induct, intrs, ...}) =
-      Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
+    val thm_name = Binding.qualified_name 
+      (Long_Name.qualify (Long_Name.base_name name) "eqvt")
+    val attr = Attrib.internal (K eqvt_add)
+    val ((_, [thm']), ctxt') =  Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
   in
-    raw_equivariance false preds raw_induct intrs ctxt 
+    (thm', ctxt')
   end
 
 fun equivariance_cmd pred_name ctxt =
   let
     val thy = ProofContext.theory_of ctxt
-    val (_, {preds, raw_induct, intrs, ...}) =
+    val ({names, ...}, {preds, raw_induct, intrs, ...}) =
       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
+     val thms = raw_equivariance preds raw_induct intrs ctxt 
   in
-    raw_equivariance true preds raw_induct intrs ctxt |> snd
+    fold_map note_named_thm (names ~~ thms) ctxt |> snd
   end
 
 local structure P = Parse and K = Keyword in