1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Fri Oct 29 16:29:39 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed Nov 03 09:45:59 2010 +0100
     1.3 @@ -463,10 +463,6 @@
     1.4     *)
     1.5  fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
     1.6      let val (pt, p) = 
     1.7 -(* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
     1.8 -   p = ([1, 9], Res);
     1.9 -   (tracing o istate2str) (get_istate pt p);
    1.10 -   *)
    1.11  	      (*locatetac is here for testing by me; step would suffice in me*)
    1.12  	    case locatetac tac (pt,p) of
    1.13  		("ok", (_, _, ptp))  => ptp
    1.14 @@ -474,9 +470,7 @@
    1.15  	      | ("not-applicable",_) => (pt, p)
    1.16  	      | ("end-of-calculation", (_, _, ptp)) => ptp
    1.17  	      | ("failure",_) => error "sys-error";
    1.18 -	val (_, ts) = 
    1.19 -(* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);
    1.20 -   *)
    1.21 +	val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
    1.22  	    (case step p ((pt, e_pos'),[]) of
    1.23  		 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
    1.24  	       | ("helpless",_) => ("helpless: cannot propose tac", [])
    1.25 @@ -484,15 +478,13 @@
    1.26  	       | ("end-of-calculation", (ts, _, _)) => ("",ts))
    1.27  	    handle _ => error "sys-error";
    1.28  	val tac = case ts of tacis as (_::_) =>
    1.29 -(* val tacis as (_::_) = ts;
    1.30 -   *)
    1.31  			     let val (tac,_,_) = last_elem tacis
    1.32  			     in tac end 
    1.33  			   | _ => if p = ([],Res) then End_Proof'
    1.34  				  else Empty_Tac;
    1.35        (*form output comes from locatetac*)
    1.36 -    in(p:pos',[]:NEW, TESTg_form (pt, p), 
    1.37 -	(tac2IDstr tac, tac):tac'_, Sundef, pt)  end;
    1.38 +    in (p:pos', []:NEW, TESTg_form (pt, p), 
    1.39 +	(tac2IDstr tac, tac):tac'_, Sundef, pt) end;
    1.40  
    1.41  (*for quick test-print-out, until 'type inout' is removed*)
    1.42  fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';