1.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Thu Aug 22 15:56:48 2019 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Thu Aug 22 16:48:04 2019 +0200
     1.3 @@ -135,18 +135,18 @@
     1.4  l = [] (* = true*);
     1.5  "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =
     1.6    (thy, ptp, E, [Celem.R], body, NONE, v);
     1.7 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
     1.8 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Program.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
     1.9    (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v);
    1.10 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Script.Try"(*1*),_) $ e), a, v) =
    1.11 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Program.Try"(*1*),_) $ e), a, v) =
    1.12    (thy, ptp, E, (l @ [Celem.L, Celem.L, Celem.R]), e1, (SOME a), v);
    1.13  (* appy thy ptp E (l @ [Celem.R]) e a v
    1.14 -ERROR WAAS: exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant "Script.Rewrite'_Set" :: ID \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool*)
    1.15 +ERROR WAAS: exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant "Program.Rewrite'_Set" :: ID \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool*)
    1.16    (* a leaf has been found *)   
    1.17  "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
    1.18    (thy, ptp, E, (l @ [Celem.R]), e, a, v);
    1.19  val (a', LTool.STac stac) = handle_leaf "next  " th sr E a v t;
    1.20  val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
    1.21 -"~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Script.Rewrite'_Set",_) $ rls $ _ $ _)) =
    1.22 +"~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Program.Rewrite'_Set",_) $ rls $ _ $ _)) =
    1.23    (pt, (Celem.assoc_thy th), stac);
    1.24  case stac2tac_ pt (Celem.assoc_thy th) stac of (Rewrite_Set "norm_equation", _) => ()
    1.25  | _ => error "stac2tac_ changed"
    1.26 @@ -156,7 +156,7 @@
    1.27  "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
    1.28        val fT = type_of f;
    1.29        val b = if put then @{term True} else @{term False};
    1.30 -      val lhs = Const ("Script.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT) 
    1.31 +      val lhs = Const ("Program.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT) 
    1.32          $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
    1.33  (*        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule.id_rls rls, idT) *)
    1.34