diff -r 0599286b1e2a -r 1264f2a21ea9 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/nominal_eqvt.ML	Wed Jun 22 12:18:22 2011 +0100
@@ -109,6 +109,7 @@
       |> map zero_var_indexes
   end
 
+
 fun note_named_thm (name, thm) ctxt = 
   let
     val thm_name = Binding.qualified_name 
@@ -124,7 +125,7 @@
     val thy = ProofContext.theory_of ctxt
     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 
+    val thms = raw_equivariance preds raw_induct intrs ctxt 
   in
     fold_map note_named_thm (names ~~ thms) ctxt |> snd
   end