src/Tools/isac/Interpret/mathengine.sml
changeset 55471 3b2a8b0d8fa9
parent 42387 767debe8a50c
child 59237 62e72f77e695
     1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Tue Jul 01 16:08:32 2014 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Tue Jul 01 16:10:52 2014 +0200
     1.3 @@ -336,19 +336,18 @@
     1.4  	   (true, pI, hdl, pbl, pre) 
     1.5      end;
     1.6  
     1.7 -(* val (pt, (pos as (p,p_):pos')) = (pt, ip);
     1.8 -   *)
     1.9  fun detailstep pt (pos as (p,p_):pos') = 
    1.10 -    let val nd = get_nd pt p
    1.11 -	val cn = children nd
    1.12 -    in if null cn 
    1.13 -       then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
    1.14 -	    then detailrls pt pos
    1.15 -	    else ("no-Rewrite_Set...", EmptyPtree, e_pos')
    1.16 -       else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
    1.17 -	     (p @ [length (children (get_nd pt p))], Res) ) 
    1.18 -    end;
    1.19 -
    1.20 +  let 
    1.21 +    val nd = get_nd pt p
    1.22 +    val cn = children nd
    1.23 +  in 
    1.24 +    if null cn 
    1.25 +    then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
    1.26 +      then detailrls pt pos
    1.27 +      else ("no-Rewrite_Set...", EmptyPtree, e_pos')
    1.28 +    else ("donesteps", pt,
    1.29 +    (p @ [length (children (get_nd pt p))], Res) ) 
    1.30 +  end;
    1.31  
    1.32  
    1.33  (***. for mathematics authoring on sml-toplevel; no XML .***)