src/Tools/isac/Interpret/mathengine.sml
changeset 59267 aab874fdd910
parent 59266 56762e8a672e
child 59269 1da53d1540fe
     1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed Dec 14 09:37:01 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed Dec 14 10:45:41 2016 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4    let
     1.5      val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
     1.6    in
     1.7 -    case f of (Ctree.Error' (Ctree.Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
     1.8 +    case f of (Ctree.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
     1.9    end
    1.10  
    1.11  (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
    1.12 @@ -368,12 +368,12 @@
    1.13      val (form, _, _) = Chead.pt_extract ptp
    1.14    in
    1.15      case form of
    1.16 -      Form t => Ctree.Form' (Ctree.FormKF (~1,Ctree.EdUndef,0,Ctree.Nundef,term2str t))
    1.17 -    | ModSpec (_,p_, _, gfr, pre, _) => 
    1.18 -      Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, 0, Ctree.Nundef, 
    1.19 -        (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method [] | _ => error "TESTg_form: uncovered case",
    1.20 - 			itms2itemppc (assoc_thy"Isac") gfr pre)))
    1.21 -   end;
    1.22 +      Form t => Ctree.FormKF (term2str t)
    1.23 +    | ModSpec (_,p_, _, gfr, pre, _) => Ctree.PpcKF (
    1.24 +        (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method []
    1.25 +        | _ => error "TESTg_form: uncovered case",
    1.26 + 			itms2itemppc (assoc_thy"Isac") gfr pre))
    1.27 +   end
    1.28  
    1.29  (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
    1.30     compare "fun CalcTree" which DOES decode                        *)
    1.31 @@ -421,6 +421,6 @@
    1.32    end
    1.33  
    1.34  (* for quick test-print-out, until 'type inout' is removed *)
    1.35 -fun f2str (Ctree.Form' (Ctree.FormKF (_, _, _, _, cterm'))) = cterm';
    1.36 +fun f2str (Ctree.FormKF cterm') = cterm';
    1.37  
    1.38  end