1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Mon May 09 10:43:43 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed May 11 07:28:13 2011 +0200
     1.3 @@ -129,32 +129,6 @@
     1.4  	           end
     1.5        end;
     1.6  
     1.7 -(*------------------------------------------------------------------
     1.8 -fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)
     1.9 -(*----------------------------------------------------from solve.sml*)
    1.10 -  | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
    1.11 -    let (*val rls = the (assoc(!ruleset',rls'))
    1.12 -	    handle _ => error ("solve: '"^rls'^"' not known");*)
    1.13 -	val thy = assoc_thy thy';
    1.14 -        val (srls, sc, is) = 
    1.15 -	    case rls of
    1.16 -		Rrls {scr=sc as Rfuns {init_state=ii,...},...} => 
    1.17 -		(e_rls, sc, RrlsState (ii t))
    1.18 -	      | Rls {srls=srls,scr=sc as Script s,...} => 
    1.19 -		(srls, sc, ScrState ([(one_scr_arg s,t)], [], 
    1.20 -			       NONE, e_term, Sundef, true));
    1.21 -	val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));
    1.22 -	val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;
    1.23 -	val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
    1.24 -	val aopt = applicable_in p pt nx;
    1.25 -    in case aopt of
    1.26 -	   Notappl s => error ("solve Detail_Set: "^s)
    1.27 -	 (* val Appl m = aopt;
    1.28 -	    *)
    1.29 -	 | Appl m => solve ("discardFIXME",m) p pt end
    1.30 -------------------------------------------------------------------*)
    1.31 -
    1.32 -
    1.33  (*iterated by nxt_me; there (the resulting) ptp dropped
    1.34    may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
    1.35  fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
    1.36 @@ -193,14 +167,8 @@
    1.37  	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
    1.38      in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
    1.39  
    1.40 -(* val ([(_, Specify_Method' (_, _, mits), _)], [],_) = 
    1.41 -    nxt_specif (Specify_Method mI) ptp;
    1.42 - *)
    1.43 -
    1.44  (*.specify a new problem;
    1.45     WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
    1.46 -(* val (pI, ptp) = (pI, (pt, ip));
    1.47 -   *)
    1.48  fun set_problem pI (ptp: ptree * pos') =
    1.49      let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
    1.50  	     _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp