1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Aug 22 09:43:43 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Aug 22 11:42:55 2021 +0200
     1.3 @@ -79,9 +79,10 @@
     1.4    if ! trace_on andalso i < ! depth 
     1.5    then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy p')
     1.6    else();
     1.7 -fun msg thy op_ thmC t = 
     1.8 - "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
     1.9 - "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
    1.10 +fun msg call thy op_ thmC t = 
    1.11 +  call ^ ": \n" ^
    1.12 +  "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
    1.13 +  "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
    1.14  
    1.15  fun rewrite__ thy i bdv tless rls put_asm thm ct =
    1.16    let
    1.17 @@ -177,7 +178,7 @@
    1.18                  let 
    1.19                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
    1.20                      ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
    1.21 -                  val _ = if pairopt <> NONE then () else raise ERROR (msg thy op_ thm' ct)
    1.22 +                  val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" thy op_ thm' ct)
    1.23                    val _ = trace_in3 i "calc. to" thy pairopt;
    1.24                  in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
    1.25              end
    1.26 @@ -281,13 +282,13 @@
    1.27      end;
    1.28  
    1.29  (* search ct for adjacent numerals and calculate them by operator isa_fn *)
    1.30 -fun calculate_ thy isa_fn ct =
    1.31 -  case Eval.adhoc_thm thy isa_fn ct of
    1.32 +fun calculate_ thy (isa_fn as (id, eval_fn)) t =
    1.33 +  case Eval.adhoc_thm thy isa_fn t of
    1.34  	  NONE => NONE
    1.35  	| SOME (thmID, thm) =>
    1.36 -	  (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
    1.37 +	  (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of
    1.38          SOME (rew, _) => rew
    1.39 -      | NONE => raise ERROR ""
    1.40 +      | NONE => raise ERROR (msg "calculate_" thy id thm t)
    1.41      in SOME (rew, (thmID, thm)) end)
    1.42  	    handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
    1.43