src/Tools/isac/Interpret/mathengine.sml
changeset 59533 aa8b25bb8ebb
parent 59416 229e5c9cf78b
child 59555 125a54fa7be0
     1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Thu Apr 04 17:29:00 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Thu Apr 04 17:52:52 2019 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4    val f2str : Generate.mout -> Rule.cterm'
     1.5  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     1.6    type nxt_
     1.7 -  type lOc_
     1.8 +  datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
     1.9    val loc_solve_ : string * Tac.tac_ -> Ctree.ctree *  Ctree.pos' -> lOc_
    1.10    val loc_specify_ : Tac.tac_ -> Ctree.state -> lOc_
    1.11    val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate'
    1.12 @@ -61,7 +61,7 @@
    1.13  | UNsafe of Chead.calcstate'   (*after loc_specify, loc_solve*)
    1.14  | Updated of Chead.calcstate'  (*after loc_specify, loc_solve*)
    1.15  
    1.16 -fun loc_specify_ m (pt,pos) =
    1.17 +fun loc_specify_ m (pt, pos) =
    1.18    let
    1.19      val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
    1.20    in