1.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Tue Jan 10 10:01:05 2023 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Tue Jan 10 17:07:53 2023 +0100
     1.3 @@ -132,7 +132,8 @@
     1.4    | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string 
     1.5      (get_calc_prog_id (Proof_Context.init_global thy) c)))
     1.6    | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id rls))
     1.7 -  | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.to_string r ^ "\"");
     1.8 +  | rule2stac thy r = raise ERROR ("rule2stac: not applicable to \"" ^
     1.9 +      Rule.to_string (Proof_Context.init_global thy) r ^ "\"");
    1.10  fun rule2stac_inst _ (Rule.Thm (thmID, _)) = 
    1.11      Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
    1.12    | rule2stac_inst thy (Rule.Eval (c, _)) = 
    1.13 @@ -141,7 +142,8 @@
    1.14      Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c)))
    1.15    | rule2stac_inst _ (Rule.Rls_ rls) = 
    1.16      Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls))
    1.17 -  | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.to_string r ^ "\"");
    1.18 +  | rule2stac_inst thy r = raise ERROR ("rule2stac_inst: not applicable to \"" ^
    1.19 +      Rule.to_string (Proof_Context.init_global thy) r ^ "\"");
    1.20  
    1.21  (*for appropriate nesting take stacs in _reverse_ order*)
    1.22  fun op #>@ sts [s] = SEq $ s $ sts