1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -167,8 +167,7 @@
     1.4                  rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
     1.5                  (* once again try the same rule, e.g. associativity against "()"*)
     1.6            | Rule.Eval (cc as (op_, _)) => 
     1.7 -            let val _= trace_in1 i "try calc" op_;
     1.8 -              val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
     1.9 +            let val _ = trace_in1 i "try calc" op_;
    1.10              in case Eval.adhoc_thm thy cc ct of
    1.11                  NONE => rew_once ruls asm ct apno thms
    1.12                | SOME (_, thm') => 
    1.13 @@ -181,8 +180,7 @@
    1.14                  in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
    1.15              end
    1.16            | Rule.Cal1 (cc as (op_, _)) => 
    1.17 -            let val _= trace_in1 i "try cal1" op_;
    1.18 -              val ct = TermC.uminus_to_string ct
    1.19 +            let val _ = trace_in1 i "try cal1" op_;
    1.20              in case Eval.adhoc_thm1_ thy cc ct of
    1.21                  NONE => (ct, asm)
    1.22                | SOME (_, thm') =>
    1.23 @@ -282,16 +280,14 @@
    1.24  
    1.25  (* search ct for adjacent numerals and calculate them by operator isa_fn *)
    1.26  fun calculate_ thy isa_fn ct =
    1.27 -  let val ct = TermC.uminus_to_string ct
    1.28 -    in case Eval.adhoc_thm thy isa_fn ct of
    1.29 -	   NONE => NONE
    1.30 -	 | SOME (thmID, thm) =>
    1.31 -	   (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
    1.32 -         SOME (rew, _) => rew
    1.33 -       | NONE => raise ERROR ""
    1.34 -     in SOME (rew, (thmID, thm)) end)
    1.35 -	   handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
    1.36 -  end;
    1.37 +  case Eval.adhoc_thm thy isa_fn ct of
    1.38 +	  NONE => NONE
    1.39 +	| SOME (thmID, thm) =>
    1.40 +	  (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
    1.41 +        SOME (rew, _) => rew
    1.42 +      | NONE => raise ERROR ""
    1.43 +    in SOME (rew, (thmID, thm)) end)
    1.44 +	    handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
    1.45  
    1.46  fun eval_prog_expr thy srls t =
    1.47    let val rew = rewrite_set_ thy false srls t;