--- a/src/Tools/code/code_funcgr.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML Sat May 17 13:54:30 2008 +0200
@@ -118,7 +118,7 @@
handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.class_error pp e ^ ",\n"
^ "for constant " ^ CodeUnit.string_of_const thy c
^ "\nin defining equations(s)\n"
- ^ (cat_lines o map string_of_thm) thms)
+ ^ (cat_lines o map Display.string_of_thm) thms)
(*handle Sorts.CLASS_ERROR _ => tab (*permissive!*)*)
end;
fun match (c, ty) = case tap_typ c
@@ -225,7 +225,7 @@
else raise CLASS_ERROR ([c], "Illegal instantation for class operation "
^ CodeUnit.string_of_const thy c
^ "\nin defining equations\n"
- ^ (cat_lines o map (string_of_thm o AxClass.overload thy)) thms)
+ ^ (cat_lines o map (Display.string_of_thm o AxClass.overload thy)) thms)
end
| NONE => (snd o CodeUnit.head_func) thm;
fun add_funcs (const, thms) =
@@ -304,7 +304,7 @@
in
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
error ("could not construct evaluation proof (probably due to wellsortedness problem):\n"
- ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
+ ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
end;
in proto_eval thy I evaluator end;