src/Tools/isac/Interpret/appl.sml
branchdecompose-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;