1.1 --- a/src/Tools/isac/Interpret/appl.sml	Wed May 04 14:07:51 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Thu May 05 09:23:32 2011 +0200
     1.3 @@ -221,36 +221,32 @@
     1.4     tests for applicability are so expensive, that results (rewrites!)
     1.5     are kept in the return-value of 'type tac_'.
     1.6  .*)
     1.7 -fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) =
     1.8 -  Appl (Init_Proof' (ct', spec))
     1.9 +fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Appl (Init_Proof' (ct', spec))
    1.10  
    1.11    | applicable_in (p,p_) pt Model_Problem = 
    1.12 -  if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
    1.13 -    then Notappl ((tac2str Model_Problem)^
    1.14 -	   " not for pos "^(pos'2str (p,p_)))
    1.15 -  else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
    1.16 -	   val {ppc,...} = get_pbt pI'
    1.17 -	   val pbl = init_pbl ppc
    1.18 -       in Appl (Model_Problem' (pI', pbl, [])) end
    1.19 -(* val Refine_Tacitly pI = m;
    1.20 -   *)
    1.21 +      if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
    1.22 +      then Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))
    1.23 +      else 
    1.24 +        let 
    1.25 +          val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
    1.26 +	        val {ppc,...} = get_pbt pI'
    1.27 +	        val pbl = init_pbl ppc
    1.28 +        in Appl (Model_Problem' (pI', pbl, [])) end
    1.29 +
    1.30    | applicable_in (p,p_) pt (Refine_Tacitly pI) = 
    1.31 -  if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
    1.32 -    then Notappl ((tac2str (Refine_Tacitly pI))^
    1.33 -	   " not for pos "^(pos'2str (p,p_)))
    1.34 -  else (* val Refine_Tacitly pI = m;
    1.35 -          *)
    1.36 -    let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
    1.37 -      val opt = refine_ori oris pI;
    1.38 -    in case opt of
    1.39 -	   SOME pblID => 
    1.40 -	   Appl (Refine_Tacitly' (pI, pblID, 
    1.41 -				  e_domID, e_metID, [](*filled in specify*)))
    1.42 -	 | NONE => Notappl ((tac2str (Refine_Tacitly pI))^
    1.43 -			    " not applicable") end
    1.44 -(* val (p,p_) = ip;
    1.45 -   val Refine_Problem pI = m;
    1.46 -   *)
    1.47 +      if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
    1.48 +      then Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))
    1.49 +      else 
    1.50 +        let 
    1.51 +          val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
    1.52 +          val opt = refine_ori oris pI;
    1.53 +        in case opt of
    1.54 +	           SOME pblID => 
    1.55 +	             Appl (Refine_Tacitly' (pI, pblID, 
    1.56 +				         e_domID, e_metID, [](*filled in specify*)))
    1.57 +	         | NONE => Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")
    1.58 +        end
    1.59 +
    1.60    | applicable_in (p,p_) pt (Refine_Problem pI) = 
    1.61    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  
    1.62      then Notappl ((tac2str (Refine_Problem pI))^