--- a/Quot/QuotMain.thy	Mon Dec 14 10:12:23 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 14 10:19:27 2009 +0100
@@ -660,7 +660,8 @@
 
 ML {*
 (* FIXME / TODO: what is asmf and asma in the code below *)
-
+(* asmf is the QUOT_TRUE assumption function
+   asma are    QUOT_TRUE assumption arguments *)
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   let