branch | decompose-isar |
changeset 41932 | a5e894d9fd8a |
parent 41928 | 20138d6136cd |
child 41933 | 8d38adf87848 |
1.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Mar 17 10:11:18 2011 +0100 1.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Mar 17 10:46:02 2011 +0100 1.3 @@ -745,6 +745,7 @@ 1.4 val pp = par_pblobj pt p; 1.5 val thy' = (get_obj g_domID pt pp):theory'; 1.6 val thy = assoc_thy thy'; 1.7 + val _ = tracing ("fun applicable_in Tac: p_ = " ^ pos_2str p_); 1.8 val f = case p_ of 1.9 Frm => get_obj g_form pt p 1.10 | Res => (fst o (get_obj g_result pt)) p;