diff -r 4a00077c008f -r 4436039cc5e1 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Fri Jul 22 11:37:16 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Fri Jul 22 11:52:12 2011 +0100
@@ -306,6 +306,7 @@
     val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt
     val p = Free (p_name, @{typ perm})
 
+    (* extracting the acc-premises from the induction theorems *)
     val acc_prems = 
      map prop_of induct_thms
      |> map2 forall_elim_list argss