src/Tools/isac/MathEngBasic/tactic.sml
changeset 59864 167472fbce77
parent 59863 0dcc8f801578
child 59865 75a9d629ea53
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Thu Apr 09 18:21:09 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 10 12:28:47 2020 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4    | rule2tac _ subst (Rule.Rls_ rls) = 
     1.5      Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.rls2str rls))
     1.6    | rule2tac _ _ rule = 
     1.7 -    error ("rule2tac: called with \"" ^ Rule_Set.rule2str rule ^ "\"");
     1.8 +    error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
     1.9  
    1.10  (* tactics for for internal use, compare "input" for user at the front-end.
    1.11    tac_ contains results from check in 'fun applicable_in'.