src/Tools/isac/Interpret/mathengine.sml
branchdecompose-isar
changeset 42067 9f1489c78cb9
parent 42011 6a9ba30ab6bc
child 42082 2556b7865f9b
     1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Thu Jun 23 15:03:21 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Tue Jun 28 15:14:00 2011 +0200
     1.3 @@ -231,10 +231,7 @@
     1.4  	    then autocalc (c@c') p (ptp,[]) (Step (s-1))
     1.5  	    else (str, c@c', ptp) end
     1.6  (*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
     1.7 -  | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=
     1.8 -(* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) = 
     1.9 -      ([], pold, get_calc cI, auto);
    1.10 -   *)
    1.11 +  | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto =
    1.12       if autoord auto > 3 andalso just_created (pt, pos)
    1.13       then let val ptp = all_modspec (pt, pos);
    1.14  	  in all_solve auto c ptp end