# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1311331932 -3600
# Node ID 4436039cc5e17b585cb3f747ec4d999758008666
# Parent  4a00077c008f85258e56ba19e15c75bd59e42dd0
tuned

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