src/Tools/isac/MathEngBasic/tactic.sml
changeset 60647 ea7db4f4f837
parent 60645 43e858cf9567
child 60655 f73460617c3d
     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 *)