1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Wed Dec 05 15:29:36 2012 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Wed Dec 05 15:56:38 2012 +0100
     1.3 @@ -104,15 +104,15 @@
     1.4  val thy' = get_obj g_domID pt (par_pblobj pt p);
     1.5  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
     1.6  "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
     1.7 -  (sc as Script (h $ body)),
     1.8 +  (sc as Prog (h $ body)),
     1.9  (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.10 -"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
    1.11 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
    1.12  (thy, ptp, sc, E, l, Skip_, a, v);
    1.13  1 < length l; (*true*)
    1.14  val up = drop_last l;
    1.15  go up sc; (* = Const ("HOL.Let", *)
    1.16 -"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
    1.17 - (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
    1.18 +"~~~~~ fun nxt_up, 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  ay = Napp_; (*false*)
    1.21  val up = drop_last l;
    1.22  val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Script.SubProblem",..*)
    1.23 @@ -291,30 +291,30 @@
    1.24            val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.25  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.26  "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
    1.27 -  (sc as Script (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.28 +  (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.29  l = []; (* = false*)
    1.30 -"~~~~~ and nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
    1.31 +"~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
    1.32    (thy, ptp, sc, E, l, Skip_, a, v);
    1.33  1 < length l; (* = true*)
    1.34  val up = drop_last l; 
    1.35  (*val (t as Abs (_,_,_)) = *)(go up sc); 
    1.36  "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) =
    1.37 -  (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
    1.38 +  (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
    1.39  term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}";
    1.40 -"~~~~~ and nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
    1.41 +"~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
    1.42    (thy, ptp, scr, E, l, ay, a, v);
    1.43  1 < length l; (* = true*)
    1.44  val up = drop_last l; 
    1.45  (*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(go up sc);
    1.46  "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay,
    1.47 -    (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
    1.48 +    (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.49  
    1.50  term2str t = "let L_La =\n      SubProblem (RatEq', [univariate, equation], [no_met])\n       [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
    1.51  
    1.52  (* comment from BEFORE Isabelle2002 --> 2011:
    1.53 -nxt_up thy ptp (Script sc) E up ay (go up sc) a v;
    1.54 +nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;
    1.55  nstep_up thy ptp scr E l ay a v;
    1.56 -nxt_up thy ptp (Script sc) E up ay (go up sc) a v;
    1.57 +nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;
    1.58  nstep_up thy ptp sc E l Skip_ a v;
    1.59  next_tac (thy',srls) (pt,pos) sc is;
    1.60  nxt_solve_ (pt,ip);