1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Mon Dec 30 11:16:00 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Wed Jan 15 11:47:38 2020 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
     1.5  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
     1.6  (*
     1.7 -WN120317.TODO dropped rateq: here "x ~= 0 should go to ctxt, but it does not:
     1.8 +WN120317.TODO dropped rateq: here "x ~= 0 should at_location to ctxt, but it does not:
     1.9   --- repair NO asms from rls RatEq_eliminate --- shows why.
    1.10  so it needs more effort to find out, how Check_elementwise worked in 2002, see below.
    1.11  *)
    1.12 @@ -109,12 +109,12 @@
    1.13  (thy, ptp, sc, E, l, Skip_, a, v);
    1.14  1 < length l; (*true*)
    1.15  val up = drop_last l;
    1.16 -go up sc; (* = Const ("HOL.Let", *)
    1.17 +at_location up sc; (* = Const ("HOL.Let", *)
    1.18  "~~~~~ fun scan_up2, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
    1.19 - (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
    1.20 + (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
    1.21  ay = Napp_; (*false*)
    1.22  val up = drop_last l;
    1.23 -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Prog_Tac.SubProblem",..*)
    1.24 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location up sc; (*Const ("Prog_Tac.SubProblem",..*)
    1.25  val i = mk_Free (i, T);
    1.26  val E = Env.update E (i, v);
    1.27  "~~~~~ fun scan_dn2, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
    1.28 @@ -297,24 +297,24 @@
    1.29    (thy, ptp, sc, E, l, Skip_, a, v);
    1.30  1 < length l; (* = true*)
    1.31  val up = drop_last l; 
    1.32 -(*val (t as Abs (_,_,_)) = *)(go up sc); 
    1.33 +(*val (t as Abs (_,_,_)) = *)(at_location up sc); 
    1.34  "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) =
    1.35 -  (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
    1.36 +  (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
    1.37  term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}";
    1.38  "~~~~~ and go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
    1.39    (thy, ptp, scr, E, l, ay, a, v);
    1.40  1 < length l; (* = true*)
    1.41  val up = drop_last l; 
    1.42 -(*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(go up sc);
    1.43 +(*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(at_location up sc);
    1.44  "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay,
    1.45 -    (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
    1.46 +    (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
    1.47  
    1.48  term2str t = "let L_La =\n      SubProblem (RatEqX, [univariate, equation], [no_met])\n       [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
    1.49  
    1.50  (* comment from BEFORE Isabelle2002 --> 2011:
    1.51 -scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v;
    1.52 +scan_up2 thy ptp (Prog sc) E up ay (at_location up sc) a v;
    1.53  go_scan_up2 thy ptp scr E l ay a v;
    1.54 -scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v;
    1.55 +scan_up2 thy ptp (Prog sc) E up ay (at_location up sc) a v;
    1.56  go_scan_up2 thy ptp sc E l Skip_ a v;
    1.57  find_next_tactic sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*);
    1.58  Step_Solve.do_next (pt,ip);