1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Jan 10 10:01:05 2023 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Jan 10 17:07:53 2023 +0100
1.3 @@ -260,7 +260,7 @@
1.4 | rule2tac ctxt subst (Rule.Rls_ rls) =
1.5 Rewrite_Set_Inst (Subst.T_to_input ctxt subst, (Rule_Set.id rls))
1.6 | rule2tac ctxt _ rule =
1.7 - raise ERROR ("rule2tac: called with \"" ^ Rule.to_string_PIDE ctxt rule ^ "\"");
1.8 + raise ERROR ("rule2tac: called with \"" ^ Rule.to_string ctxt rule ^ "\"");
1.9
1.10 (* try if a rewrite-rule is applicable to a given formula;
1.11 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)