1.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Tue Jan 10 10:01:05 2023 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Tue Jan 10 17:07:53 2023 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4  fun of_thm thm = (id_of_thm thm, thm);
     1.5  fun from_rule _ (Rule.Thm (id, thm)) = (id, thm)
     1.6    | from_rule ctxt r =
     1.7 -    raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r);
     1.8 +    raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string ctxt r);
     1.9  
    1.10  \<^isac_test>\<open>
    1.11  fun string_of_thm_in_thy thy thm =
    1.12 @@ -151,7 +151,7 @@
    1.13          | _ => "sym_" ^ thmID
    1.14        in Rule.Thm (thmID', thm') end
    1.15    | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
    1.16 -  | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^  Rule.to_string_PIDE ctxt r)
    1.17 +  | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^  Rule.to_string ctxt r)
    1.18  
    1.19  \<^isac_test>\<open>
    1.20  (* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)
    1.21 @@ -167,7 +167,7 @@
    1.22        else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)
    1.23    | revert_sym_rule thy rule =
    1.24      raise ERROR ("ThmC.revert_sym_rule: NOT for " ^
    1.25 -      Rule.to_string_PIDE (Proof_Context.init_global thy) rule)
    1.26 +      Rule.to_string (Proof_Context.init_global thy) rule)
    1.27  \<close>
    1.28  
    1.29