1.1 --- a/src/Pure/Isar/code.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4  (** certificate theorems **)
     1.5  
     1.6  fun string_of_lthms r = case Susp.peek r
     1.7 - of SOME thms => (map string_of_thm o rev) thms
     1.8 + of SOME thms => (map Display.string_of_thm o rev) thms
     1.9    | NONE => ["[...]"];
    1.10  
    1.11  fun pretty_lthms ctxt r = case Susp.peek r
    1.12 @@ -147,7 +147,7 @@
    1.13        | matches (_ :: _) [] = false
    1.14        | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
    1.15      fun drop thm' = not (matches args (args_of thm'))
    1.16 -      orelse (warning ("code generator: dropping redundant defining equation\n" ^ string_of_thm thm'); false);
    1.17 +      orelse (warning ("code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); false);
    1.18      val (keeps, drops) = List.partition drop sels;
    1.19    in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end;
    1.20  
    1.21 @@ -537,7 +537,7 @@
    1.22    let
    1.23      fun cert thm = if const = const_of_func thy thm
    1.24        then thm else error ("Wrong head of defining equation,\nexpected constant "
    1.25 -        ^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm)
    1.26 +        ^ CodeUnit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
    1.27    in map cert thms end;
    1.28  
    1.29  
    1.30 @@ -655,13 +655,13 @@
    1.31              then thm
    1.32              else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty
    1.33                ^ "\nof defining equation\n"
    1.34 -              ^ string_of_thm thm
    1.35 +              ^ Display.string_of_thm thm
    1.36                ^ "\nto permitted most general type\n"
    1.37                ^ CodeUnit.string_of_typ thy ty_decl);
    1.38                constrain thm)
    1.39              else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
    1.40                ^ "\nof defining equation\n"
    1.41 -              ^ string_of_thm thm
    1.42 +              ^ Display.string_of_thm thm
    1.43                ^ "\nis incompatible with permitted least general type\n"
    1.44                ^ CodeUnit.string_of_typ thy ty_strongest)
    1.45            end;
    1.46 @@ -673,7 +673,7 @@
    1.47          then thm
    1.48          else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
    1.49             ^ "\nof defining equation\n"
    1.50 -           ^ string_of_thm thm
    1.51 +           ^ Display.string_of_thm thm
    1.52             ^ "\nis incompatible with declared function type\n"
    1.53             ^ CodeUnit.string_of_typ thy ty_decl)
    1.54        end;
    1.55 @@ -731,11 +731,11 @@
    1.56      val c = const_of_func thy func;
    1.57      val _ = if (is_some o AxClass.class_of_param thy) c
    1.58        then error ("Rejected polymorphic equation for overloaded constant:\n"
    1.59 -        ^ string_of_thm thm)
    1.60 +        ^ Display.string_of_thm thm)
    1.61        else ();
    1.62      val _ = if (is_some o get_datatype_of_constr thy) c
    1.63        then error ("Rejected equation for datatype constructor:\n"
    1.64 -        ^ string_of_thm func)
    1.65 +        ^ Display.string_of_thm func)
    1.66        else ();
    1.67    in
    1.68      (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default