1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  fun rewrite__ thy i bdv tless rls put_asm thm ct =
     1.5    let
     1.6      val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
     1.7 -		  (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct
     1.8 +		  (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct
     1.9    in if rew then SOME (t', distinct asms) else NONE end
    1.10    (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
    1.11  and rew_sub thy i bdv tless rls put_asm lrd r t = 
    1.12 @@ -125,14 +125,14 @@
    1.13        val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
    1.14  	    val (t', asm, rew) = app_rev thy (i + 1) rrls t                   
    1.15      in if rew then SOME (t', distinct asm) else NONE end
    1.16 -  | rewrite__set_ thy i put_asm bdv rls ct =          (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
    1.17 +  | rewrite__set_ thy i put_asm bdv rls ct =          (* Rls, Seq containing Thms or Eval, Cal1 *)
    1.18      let
    1.19        (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
    1.20        datatype switch = Appl | Noap;
    1.21        fun rew_once _ asm ct Noap [] = (ct, asm)         (* ?TODO unify with Prog_Expr.rew_once? *)
    1.22          | rew_once ruls asm ct Appl [] = 
    1.23            (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
    1.24 -          | Rule_Set.Seqence _ => (ct, asm)
    1.25 +          | Rule_Set.Sequence _ => (ct, asm)
    1.26            | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
    1.27          | rew_once ruls asm ct apno (rul :: thms) =
    1.28            case rul of
    1.29 @@ -145,10 +145,10 @@
    1.30                  (trace1 i (" rewrites to: \"" ^ UnparseC.term_in_thy thy ct' ^ "\"");
    1.31                  rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
    1.32                  (* once again try the same rule, e.g. associativity against "()"*)
    1.33 -          | Rule.Num_Calc (cc as (op_, _)) => 
    1.34 +          | Rule.Eval (cc as (op_, _)) => 
    1.35              let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
    1.36                val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
    1.37 -            in case Num_Calc.adhoc_thm thy cc ct of
    1.38 +            in case Eval.adhoc_thm thy cc ct of
    1.39                  NONE => rew_once ruls asm ct apno thms
    1.40                | SOME (_, thm') => 
    1.41                  let 
    1.42 @@ -162,7 +162,7 @@
    1.43            | Rule.Cal1 (cc as (op_, _)) => 
    1.44              let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
    1.45                val ct = TermC.uminus_to_string ct
    1.46 -            in case Num_Calc.adhoc_thm1_ thy cc ct of
    1.47 +            in case Eval.adhoc_thm1_ thy cc ct of
    1.48                  NONE => (ct, asm)
    1.49                | SOME (_, thm') =>
    1.50                  let 
    1.51 @@ -262,7 +262,7 @@
    1.52  (* search ct for adjacent numerals and calculate them by operator isa_fn *)
    1.53  fun calculate_ thy isa_fn ct =
    1.54    let val ct = TermC.uminus_to_string ct
    1.55 -    in case Num_Calc.adhoc_thm thy isa_fn ct of
    1.56 +    in case Eval.adhoc_thm thy isa_fn ct of
    1.57  	   NONE => NONE
    1.58  	 | SOME (thmID, thm) =>
    1.59  	   (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of