src/Sequents/simpdata.ML

                       (Const("equal",_)$_$_)   => th RS @{thm eq_reflection}
                     | (Const("iff",_)$_$_) => th RS @{thm iff_reflection}
                     | (Const("Not",_)$_)      => th RS iff_reflection_F
                     | _                       => th RS iff_reflection_T)
            | _ => error ("addsimps: unable to use theorem\n" ^
-                         string_of_thm th));
+                         Display.string_of_thm th));
 
 (*Replace premises x=y, X<->Y by X==Y*)
 val mk_meta_prems =
     rule_by_tactic
       (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));