src/Tools/Code/code_thingol.ML
changeset 32131 7913823f14e3
parent 32123 8bac9ee4b28d
parent 32091 30e2ffbba718
child 32273 3c395fc7ec5e
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 22 10:49:26 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 22 11:23:09 2009 +0200
     1.3 @@ -469,7 +469,7 @@
     1.4    let
     1.5      val err_class = Sorts.class_error (Syntax.pp_global thy) e;
     1.6      val err_thm = case thm
     1.7 -     of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
     1.8 +     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
     1.9      val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
    1.10        ^ Syntax.string_of_sort_global thy sort;
    1.11    in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;