1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4  val SOME (t,_) = 
     1.5      rewrite_inst_ thy e_rew_ord 
     1.6  		  (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty 
     1.7 -			      [(Num_Calc ("EqSystem.occur'_exactly'_in", 
     1.8 +			      [(Eval ("EqSystem.occur'_exactly'_in", 
     1.9  				      eval_occur_exactly_in 
    1.10  					  "#eval_occur_exactly_in_"))
    1.11  			       ]) 
    1.12 @@ -310,7 +310,7 @@
    1.13  val thm = @{thm rat_mult_poly_r};
    1.14           "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
    1.15  val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty 
    1.16 -                      [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
    1.17 +                      [Eval ("Poly.is'_polyexp", eval_is_polyexp "")];
    1.18  val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
    1.19  (*t' = t''; (*false because of further rewrites in t'*)*)
    1.20  "----- rew_sub  --------------------------------";
    1.21 @@ -395,7 +395,7 @@
    1.22  val pres = [parse_patt thy "?p is_multUnordered"];
    1.23  val prepat = [(pres, pat)];
    1.24  val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
    1.25 -		      [Num_Calc ("Poly.is'_multUnordered", 
    1.26 +		      [Eval ("Poly.is'_multUnordered", 
    1.27                               eval_is_multUnordered "")];
    1.28  
    1.29  val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
    1.30 @@ -529,7 +529,7 @@
    1.31        fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
    1.32          | rew_once ruls asm ct Appl [] = 
    1.33            (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
    1.34 -          | Rule_Set.Seqence _ => (ct, asm)
    1.35 +          | Rule_Set.Sequence _ => (ct, asm)
    1.36            | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
    1.37          | rew_once ruls asm ct apno (rul :: thms) =
    1.38            case rul of
    1.39 @@ -542,10 +542,10 @@
    1.40                  (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
    1.41                  rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
    1.42                  (* once again try the same rule, e.g. associativity against "()"*)
    1.43 -          | Rule.Num_Calc (cc as (op_, _)) => 
    1.44 +          | Rule.Eval (cc as (op_, _)) => 
    1.45              let val _= trace1 i (" try calc: " ^ op_ ^ "'")
    1.46                val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
    1.47 -            in case Num_Calc.adhoc_thm thy cc ct of
    1.48 +            in case Eval.adhoc_thm thy cc ct of
    1.49                  NONE => rew_once ruls asm ct apno thms
    1.50                | SOME (_, thm') => 
    1.51                  let 
    1.52 @@ -559,7 +559,7 @@
    1.53            | Rule.Cal1 (cc as (op_, _)) => 
    1.54              let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
    1.55                val ct = TermC.uminus_to_string ct
    1.56 -            in case Num_Calc.adhoc_thm1_ thy cc ct of
    1.57 +            in case Eval.adhoc_thm1_ thy cc ct of
    1.58                  NONE => (ct, asm)
    1.59                | SOME (_, thm') =>
    1.60                  let 
    1.61 @@ -591,10 +591,10 @@
    1.62  
    1.63      val (t', asms, _ (*lrd*), rew) =
    1.64             rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
    1.65 -		  (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct;
    1.66 +		  (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct;
    1.67  "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
    1.68    = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
    1.69 -		  (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
    1.70 +		  (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm), ct);
    1.71      val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
    1.72      val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
    1.73  ;
    1.74 @@ -641,15 +641,15 @@
    1.75  
    1.76  (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
    1.77  (*+*)(*val rules =
    1.78 -(*+*)   [Num_Calc ("Rings.divide_class.divide", fn),
    1.79 +(*+*)   [Eval ("Rings.divide_class.divide", fn),
    1.80  (*+*)    Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
    1.81  (*+*)    :
    1.82 -(*+*)    Num_Calc ("HOL.eq", fn),
    1.83 +(*+*)    Eval ("HOL.eq", fn),
    1.84  (*+*)    Thm ("not_true", "(\<not> True) = False"),
    1.85  (*+*)    Thm ("not_false", "(\<not> False) = True"),
    1.86  (*+*)    :
    1.87 -(*+*)    Num_Calc ("Prog_Expr.pow", fn),
    1.88 -(*+*)    Num_Calc ("RatEq.is'_ratequation'_in", fn)]:
    1.89 +(*+*)    Eval ("Prog_Expr.pow", fn),
    1.90 +(*+*)    Eval ("RatEq.is'_ratequation'_in", fn)]:
    1.91  (*+*)   rule list*)
    1.92  (*+*)chk: term list -> term list -> term list * bool
    1.93