src/Tools/Code/code_thingol.ML

   if permissive
   then raise PERMISSIVE ()
   else
     let
       val thm_msg =
-        Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
+        Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm;
       val dep_msg = if null (tl deps) then NONE
         else SOME ("with dependency "
           ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps)));
       val thm_dep_msg = case (thm_msg, dep_msg)
        of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")"