--- a/Nominal-General/nominal_eqvt.ML	Tue Jun 01 15:01:05 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Tue Jun 01 15:21:01 2010 +0200
@@ -10,7 +10,7 @@
   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: term list -> thm -> thm list -> Proof.context -> thm list * local_theory
+  val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
   val equivariance_cmd: string -> Proof.context -> local_theory
 end
 
@@ -147,7 +147,7 @@
   (thm', ctxt')
 end
 
-fun equivariance pred_trms raw_induct intrs ctxt = 
+fun equivariance note_flag pred_trms raw_induct intrs ctxt = 
 let
   val is_already_eqvt = 
     filter (is_eqvt ctxt) pred_trms
@@ -172,7 +172,9 @@
     |> singleton (ProofContext.export ctxt' ctxt))
   val thms' = map (fn th => zero_var_indexes (th RS mp)) thms
 in
-  ctxt |> fold_map note_named_thm (pred_names ~~ thms')   
+  if note_flag
+  then ctxt |> fold_map note_named_thm (pred_names ~~ thms')  
+  else (thms', ctxt) 
 end
 
 fun equivariance_cmd pred_name ctxt =
@@ -181,7 +183,7 @@
   val (_, {preds, raw_induct, intrs, ...}) =
     Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
 in
-  equivariance preds raw_induct intrs ctxt |> snd
+  equivariance true preds raw_induct intrs ctxt |> snd
 end
 
 local structure P = Parse and K = Keyword in