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" ?*)