test/Tools/isac/Knowledge/algein.sml
changeset 59253 f0bb15a046ae
parent 59248 5eba5e6d5266
child 59395 862eb17f9e16
     1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -73,9 +73,11 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
     1.5  val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
     1.6  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.7 -if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
     1.8 -else error "algein.sml diff.behav. in erstSymbolisch 99";
     1.9 - DEconstrCalcTree 1;
    1.10 +if f2str f = "L = 104"
    1.11 +then case nxt of ("End_Proof'", End_Proof') => ()
    1.12 +  | _ => error "algein.sml diff.behav. in erstSymbolisch 99 1"
    1.13 +else error "algein.sml diff.behav. in erstSymbolisch 99 2";
    1.14 +DEconstrCalcTree 1;
    1.15  
    1.16  "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
    1.17  "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";