src/Pure/Isar/code.ML

 
 
 (** certificate theorems **)
 
 fun string_of_lthms r = case Susp.peek r
- of SOME thms => (map string_of_thm o rev) thms
+ of SOME thms => (map Display.string_of_thm o rev) thms
   | NONE => ["[...]"];
 
 fun pretty_lthms ctxt r = case Susp.peek r
  of SOME thms => map (ProofContext.pretty_thm ctxt) thms
   | NONE => [Pretty.str "[...]"];

     fun matches [] _ = true
       | matches (Var _ :: xs) [] = matches xs []
       | matches (_ :: _) [] = false
       | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
     fun drop thm' = not (matches args (args_of thm'))
-      orelse (warning ("code generator: dropping redundant defining equation\n" ^ string_of_thm thm'); false);
+      orelse (warning ("code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); false);
     val (keeps, drops) = List.partition drop sels;
   in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end;
 
 fun add_thm thm (sels, dels) =
   apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));

 
 fun certify_const thy const thms =
   let
     fun cert thm = if const = const_of_func thy thm
       then thm else error ("Wrong head of defining equation,\nexpected constant "
-        ^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm)
+        ^ CodeUnit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
   in map cert thms end;
 
 
 
 (** operational sort algebra and class discipline **)

           in if Sign.typ_instance thy (ty_strongest, ty)
             then if Sign.typ_instance thy (ty, ty_decl)
             then thm
             else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty
               ^ "\nof defining equation\n"
-              ^ string_of_thm thm
+              ^ Display.string_of_thm thm
               ^ "\nto permitted most general type\n"
               ^ CodeUnit.string_of_typ thy ty_decl);
               constrain thm)
             else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
               ^ "\nof defining equation\n"
-              ^ string_of_thm thm
+              ^ Display.string_of_thm thm
               ^ "\nis incompatible with permitted least general type\n"
               ^ CodeUnit.string_of_typ thy ty_strongest)
           end;
     fun check_typ_fun (c, thm) =
       let

         val ty_decl = Sign.the_const_type thy c;
       in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
         then thm
         else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
            ^ "\nof defining equation\n"
-           ^ string_of_thm thm
+           ^ Display.string_of_thm thm
            ^ "\nis incompatible with declared function type\n"
            ^ CodeUnit.string_of_typ thy ty_decl)
       end;
     fun check_typ (c, thm) =
       case AxClass.inst_of_param thy c

   let
     val func = mk_func thm;
     val c = const_of_func thy func;
     val _ = if (is_some o AxClass.class_of_param thy) c
       then error ("Rejected polymorphic equation for overloaded constant:\n"
-        ^ string_of_thm thm)
+        ^ Display.string_of_thm thm)
       else ();
     val _ = if (is_some o get_datatype_of_constr thy) c
       then error ("Rejected equation for datatype constructor:\n"
-        ^ string_of_thm func)
+        ^ Display.string_of_thm func)
       else ();
   in
     (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
       (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy
   end;