1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Thu Nov 21 15:31:32 2019 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Nov 25 16:39:52 2019 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4      val assoc_thm'': theory -> Celem.thmID -> thm
     1.5      val calculate_: theory -> string * Rule.eval_fn -> term -> (term * (string * thm)) option
     1.6      val eval__true: theory -> int -> term list -> (term * term) list -> Rule.rls -> term list * bool
     1.7 -    val eval_listexpr_: theory -> Rule.rls -> term -> term
     1.8 +    val eval_prog_expr: theory -> Rule.rls -> term -> term
     1.9      val eval_true: theory -> term list -> Rule.rls -> bool
    1.10      val eval_true_: Rule.theory' -> Rule.rls -> term -> bool
    1.11      val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
    1.12 @@ -321,7 +321,7 @@
    1.13    ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => 
    1.14      error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ Rule.theory2domID thy ^ "\" (and parents)")
    1.15  
    1.16 -fun eval_listexpr_ thy srls t =
    1.17 +fun eval_prog_expr thy srls t =
    1.18    let val rew = rewrite_set_ thy false srls t;
    1.19    in case rew of SOME (res,_) => res | NONE => t end;
    1.20