src/Tools/isac/Interpret/mathengine.sml
branchdecompose-isar
changeset 42305 3ff2cf70f845
parent 42082 2556b7865f9b
child 42387 767debe8a50c
     1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Fri Oct 07 16:54:31 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Tue Oct 11 10:59:42 2011 +0200
     1.3 @@ -188,8 +188,8 @@
     1.4  fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
     1.5    let val pIopt = get_pblID (pt,ip);
     1.6    in
     1.7 -    if (*p = ([],Res) orelse*) ip = ([],Res)
     1.8 -    then ("end-of-calculation",(tacis, [], ptp):calcstate') 
     1.9 +    if ip = ([],Res)
    1.10 +    then ("end-of-calculation", (tacis, [], ptp):calcstate') 
    1.11      else
    1.12        case tacis of
    1.13  	      (_::_) => 
    1.14 @@ -393,7 +393,7 @@
    1.15      val (pt, p) = 
    1.16  	    (*locatetac is here for testing by me; step would suffice in me*)
    1.17  	    case locatetac tac (pt,p) of
    1.18 -		    ("ok", (_, _, ptp))  => ptp
    1.19 +		    ("ok", (_, _, ptp)) => ptp
    1.20  	    | ("unsafe-ok", (_, _, ptp)) => ptp
    1.21  	    | ("not-applicable",_) => (pt, p)
    1.22  	    | ("end-of-calculation", (_, _, ptp)) => ptp