1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Sat Aug 21 18:58:33 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Aug 22 09:43:43 2021 +0200
     1.3 @@ -79,6 +79,9 @@
     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  
    1.11  fun rewrite__ thy i bdv tless rls put_asm thm ct =
    1.12    let
    1.13 @@ -139,23 +142,23 @@
    1.14              (*asm false .. thm not applied ^^^; continue until False vvv*)
    1.15              else chk (indets @ [t] @ a') asms);
    1.16        in chk [] asms end
    1.17 -and rewrite__set_ thy _ _ _ Rule_Set.Empty t =                         (* rewrite with a rule set*)
    1.18 +and rewrite__set_ thy (*1*)_ _ _ Rule_Set.Empty t =                         (* rewrite with a rule set*)
    1.19      raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
    1.20 -  | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t =    (* rewrite with a 'reverse rule set'*)
    1.21 +  | rewrite__set_ (*2*)thy i _ _ (rrls as Rule_Set.Rrls _) t =    (* rewrite with a 'reverse rule set'*)
    1.22      let
    1.23        val _= trace_eq1 i "rls" rrls thy t;
    1.24  	    val (t', asm, rew) = app_rev thy (i + 1) rrls t                   
    1.25      in if rew then SOME (t', distinct op = asm) else NONE end
    1.26 -  | rewrite__set_ thy i put_asm bdv rls ct =           (* Rls, Seq containing Thms or Eval, Cal1 *)
    1.27 +  | rewrite__set_ (*3*)thy i put_asm bdv rls ct =           (* Rls, Seq containing Thms or Eval, Cal1 *)
    1.28      let
    1.29        (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
    1.30        datatype switch = Appl | Noap;
    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 +      fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
    1.34 +        | rew_once (*2*)ruls asm ct Appl [] = 
    1.35            (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
    1.36            | Rule_Set.Sequence _ => (ct, asm)
    1.37            | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
    1.38 -        | rew_once ruls asm ct apno (rul :: thms) =
    1.39 +        | rew_once (*3*)ruls asm ct apno (rul :: thms) =
    1.40            case rul of
    1.41              Rule.Thm (thmid, thm) =>
    1.42                (trace_in1 i "try thm" thmid;
    1.43 @@ -174,8 +177,7 @@
    1.44                  let 
    1.45                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
    1.46                      ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
    1.47 -                  val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ 
    1.48 -                    ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
    1.49 +                  val _ = if pairopt <> NONE then () else raise ERROR (msg thy op_ thm' ct)
    1.50                    val _ = trace_in3 i "calc. to" thy pairopt;
    1.51                  in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
    1.52              end