test/Tools/isac/Interpret/ctree.sml
changeset 59253 f0bb15a046ae
parent 59248 5eba5e6d5266
child 59267 aab874fdd910
     1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -132,8 +132,10 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
     1.5  val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
     1.6  val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
     1.7 -if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
     1.8 -else error "new behaviour in test: miniscript with mini-subpbl";
     1.9 +if res = "[x = 1]"
    1.10 +then case nxt of ("End_Proof'", End_Proof') => ()
    1.11 +  | _ => error "new behaviour in test: miniscript with mini-subpbl 1"
    1.12 +else error "new behaviour in test: miniscript with mini-subpbl 2" 
    1.13  
    1.14   show_pt pt;
    1.15