test/Tools/isac/Knowledge/polyminus.sml
changeset 59749 cc3b1807f72e
parent 59747 8e5335c63475
child 59773 d88bb023c380
     1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Thu Dec 19 12:40:17 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Dec 19 16:41:57 2019 +0100
     1.3 @@ -263,8 +263,9 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.5  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.6  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.7 -if f2str f = "3 - 2 * e + 2 * f + 2 * g" andalso #1 nxt = "End_Proof'" then ()
     1.8 -else error "polyminus.sml: me simplification.for_polynomials.with_minus";
     1.9 +if f2str f = "3 - 2 * e + 2 * f + 2 * g" 
    1.10 +then case nxt of End_Proof' => () | _ =>  error "me simplification.for_polynomials.with_minus 1"
    1.11 +else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
    1.12  
    1.13  "----------- pbl polynom vereinfachen p.33 -----------------------";
    1.14  "----------- pbl polynom vereinfachen p.33 -----------------------";