src/HOL/Tools/lin_arith.ML

 (* to the proof state                                                        *)
 (*---------------------------------------------------------------------------*)
 
 (* checks if splitting with 'thm' is implemented                             *)
 
-fun is_split_thm (thm : thm) : bool =
+fun is_split_thm thm =
   case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
     (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
     case head_of lhs of
       Const (a, _) => member (op =) [@{const_name Orderings.max},
                                     @{const_name Orderings.min},

                                     @{const_name HOL.minus},
                                     "Int.nat",
                                     "Divides.div_class.mod",
                                     "Divides.div_class.div"] a
     | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
-                                 Display.string_of_thm thm);
+                                 Display.string_of_thm_without_context thm);
                        false))
   | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
-                   Display.string_of_thm thm);
+                   Display.string_of_thm_without_context thm);
           false);
 
 (* substitute new for occurrences of old in a term, incrementing bound       *)
 (* variables as needed when substituting inside an abstraction               *)