1.1 --- a/src/Tools/isac/Interpret/appl.sml	Sun May 15 11:32:41 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sun May 15 12:36:29 2011 +0200
     1.3 @@ -594,59 +594,48 @@
     1.4  ------------------*)
     1.5  
     1.6    | applicable_in p pt (Apply_Assumption cts') = 
     1.7 -  (error ("applicable_in: not impl. for "^
     1.8 -	       (tac2str (Apply_Assumption cts'))))
     1.9 +      (error ("applicable_in: not impl. for " ^ (tac2str (Apply_Assumption cts'))))
    1.10    
    1.11    (*'logical' applicability wrt. script in locate: Inconsistent?*)
    1.12    | applicable_in (p,p_) pt (m as Take ct') = 
    1.13 -     if member op = [Pbl,Met] p_ 
    1.14 -       then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.15 -     else
    1.16 -       let val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.17 -       in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
    1.18 -	       SOME ct => Appl (Take' ct)
    1.19 -	     | NONE => Notappl ("syntax error in "^ct'))
    1.20 -       end
    1.21 +      if member op = [Pbl,Met] p_ 
    1.22 +      then Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))
    1.23 +      else
    1.24 +        let val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.25 +        in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
    1.26 +	            SOME ct => Appl (Take' ct)
    1.27 +	          | NONE => Notappl ("syntax error in " ^ ct'))
    1.28 +        end
    1.29  
    1.30    | applicable_in p pt (Take_Inst ct') = 
    1.31 -  error ("applicable_in: not impl. for "^
    1.32 -	       (tac2str (Take_Inst ct')))
    1.33 -
    1.34 +      error ("applicable_in: not impl. for " ^ tac2str (Take_Inst ct'))
    1.35    | applicable_in p pt (Group (con, ints)) = 
    1.36 -  error ("applicable_in: not impl. for "^
    1.37 -	       (tac2str (Group (con, ints))))
    1.38 +      error ("applicable_in: not impl. for " ^ tac2str (Group (con, ints)))
    1.39  
    1.40    | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) = 
    1.41       if member op = [Pbl,Met] p_
    1.42 -       then (*maybe Apply_Method has already been done*)
    1.43 -	 case get_obj g_env pt p of
    1.44 -	     SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [], 
    1.45 -					   e_term, [], e_ctxt, subpbl domID pblID))
    1.46 -	   | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.47 +     then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
    1.48 +	      case get_obj g_env pt p of
    1.49 +	        SOME is => 
    1.50 +            Appl (Subproblem' ((domID, pblID, e_metID), [], 
    1.51 +					    e_term, [], e_ctxt(*FIXME.WN150511*), subpbl domID pblID))
    1.52 +	      | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.53       else (*somewhere later in the script*)
    1.54         Appl (Subproblem' ((domID, pblID, e_metID), [], 
    1.55 -			  e_term, [], e_ctxt, subpbl domID pblID))
    1.56 +			   e_term, [], e_ctxt, subpbl domID pblID))
    1.57  
    1.58    | applicable_in p pt (End_Subproblem) =
    1.59 -  error ("applicable_in: not impl. for "^
    1.60 -	       (tac2str (End_Subproblem)))
    1.61 -
    1.62 +      error ("applicable_in: not impl. for " ^ tac2str End_Subproblem)
    1.63    | applicable_in p pt (CAScmd ct') = 
    1.64 -  error ("applicable_in: not impl. for "^
    1.65 -	       (tac2str (CAScmd ct')))
    1.66 -  
    1.67 +      error ("applicable_in: not impl. for " ^ tac2str (CAScmd ct'))  
    1.68    | applicable_in p pt (Split_And) = 
    1.69 -  error ("applicable_in: not impl. for "^
    1.70 -	       (tac2str (Split_And)))
    1.71 +      error ("applicable_in: not impl. for " ^ tac2str Split_And)
    1.72    | applicable_in p pt (Conclude_And) = 
    1.73 -  error ("applicable_in: not impl. for "^
    1.74 -	       (tac2str (Conclude_And)))
    1.75 +      error ("applicable_in: not impl. for " ^ tac2str Conclude_And)
    1.76    | applicable_in p pt (Split_Or) = 
    1.77 -  error ("applicable_in: not impl. for "^
    1.78 -	       (tac2str (Split_Or)))
    1.79 +      error ("applicable_in: not impl. for " ^ tac2str Split_Or)
    1.80    | applicable_in p pt (Conclude_Or) = 
    1.81 -  error ("applicable_in: not impl. for "^
    1.82 -	       (tac2str (Conclude_Or)))
    1.83 +      error ("applicable_in: not impl. for " ^ tac2str Conclude_Or)
    1.84  
    1.85    | applicable_in (p,p_) pt (Begin_Trans) =
    1.86      let