1.1 --- a/test/Tools/isac/ProgLang/prog-tools.sml	Thu Nov 21 15:31:32 2019 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/prog-tools.sml	Mon Nov 25 16:39:52 2019 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
     1.5  "-------- distinguish input to Model -----------------------------------------";
     1.6  "-------- fun subpbl, fun pblterm --------------------------------------------";
     1.7 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
     1.8 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
     1.9  "-------- fun is_calc, fun op_of_calc ----------------------------------------";
    1.10  "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
    1.11  "-------- fun op #> ----------------------------------------------------------";
    1.12 @@ -175,9 +175,9 @@
    1.13  init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) 
    1.14  			      (str2term "someTermWithBdv");
    1.15  
    1.16 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
    1.17 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
    1.18 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
    1.19 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
    1.20 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
    1.21 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
    1.22  val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
    1.23  case stacpbls sc of
    1.24    [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
    1.25 @@ -205,8 +205,8 @@
    1.26  @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
    1.27  case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
    1.28  
    1.29 -(* --- fun subst_stacexpr *)
    1.30 -case  subst_stacexpr [] NONE e_term  sc of
    1.31 +(* --- fun eval_leaf *)
    1.32 +case  eval_leaf [] NONE e_term  sc of
    1.33  (NONE, Expr (Const ("HOL.eq", _) $
    1.34   (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
    1.35    (Const ("HOL.Let", _) $
    1.36 @@ -217,7 +217,7 @@
    1.37        Free ("e_e", _)) $
    1.38      Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
    1.39  )) => ()
    1.40 -| _ => error "subst_stacexpr [] NONE e_term";
    1.41 +| _ => error "eval_leaf [] NONE e_term";
    1.42  
    1.43  "-------- fun is_calc, fun op_of_calc ----------------------------------------";
    1.44  "-------- fun is_calc, fun op_of_calc ----------------------------------------";