diff -r ca6aac81b893 -r a5e894d9fd8a src/Tools/isac/Interpret/appl.sml
--- a/src/Tools/isac/Interpret/appl.sml	Thu Mar 17 10:11:18 2011 +0100
+++ b/src/Tools/isac/Interpret/appl.sml	Thu Mar 17 10:46:02 2011 +0100
@@ -745,6 +745,7 @@
     val pp = par_pblobj pt p; 
     val thy' = (get_obj g_domID pt pp):theory';
     val thy = assoc_thy thy';
+    val _ = tracing ("fun applicable_in Tac: p_ = " ^ pos_2str p_);
     val f = case p_ of
               Frm => get_obj g_form pt p
 	    | Res => (fst o (get_obj g_result pt)) p;