1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Mar 17 10:46:02 2011 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri Mar 18 09:26:03 2011 +0100
     1.3 @@ -740,14 +740,14 @@
     1.4    | applicable_in p pt (Empty_Tac) = 
     1.5    Notappl "Empty_Tac is not applicable"
     1.6  
     1.7 -  | applicable_in (p,p_) pt (Tac id) = 
     1.8 +  | applicable_in (p,p_) pt (Tac id) =
     1.9    let 
    1.10      val pp = par_pblobj pt p; 
    1.11      val thy' = (get_obj g_domID pt pp):theory';
    1.12      val thy = assoc_thy thy';
    1.13 -    val _ = tracing ("fun applicable_in Tac: p_ = " ^ pos_2str p_);
    1.14      val f = case p_ of
    1.15                Frm => get_obj g_form pt p
    1.16 +            | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
    1.17  	    | Res => (fst o (get_obj g_result pt)) p;
    1.18    in case id of
    1.19        "subproblem_equation_dummy" =>