test/Tools/isac/Knowledge/rateq.sml
changeset 59585 0bb418c3855a
parent 59583 cfc0dd8b6849
child 59601 0cff71323cdd
     1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Thu Aug 22 15:56:48 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Thu Aug 22 16:48:04 2019 +0200
     1.3 @@ -115,14 +115,14 @@
     1.4   (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
     1.5  ay = Napp_; (*false*)
     1.6  val up = drop_last l;
     1.7 -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Script.SubProblem",..*)
     1.8 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Program.SubProblem",..*)
     1.9  val i = mk_Free (i, T);
    1.10  val E = upd_env E (i, v);
    1.11  "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
    1.12    (thy, ptp, E, (up@[R,D]), body, a, v);
    1.13  "~~~~~ fun handle_leaf, args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t);
    1.14  "~~~~~ fun subst_stacexpr, args:"; val (E, a, v, 
    1.15 -	  (t as (Const ("Script.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
    1.16 +	  (t as (Const ("Program.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
    1.17  val STac tm = STac (subst_atomic E t);
    1.18  term2str tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
    1.19  (*                                     ------ ^^^ ----- ? "x" ?*)