src/Pure/axclass.ML
changeset 32197 bc341bbe4417
parent 31948 ea8c8bf47ce3
child 32765 3032c0308019
--- a/src/Pure/axclass.ML	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/Pure/axclass.ML	Sun Jul 26 13:12:52 2009 +0200
@@ -607,8 +607,10 @@
     val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
     val ths =
       sort |> map (fn c =>
-        Goal.finish (the (lookup_type cache' typ c) RS
-          Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
+        Goal.finish
+          (Syntax.init_pretty_global thy)
+          (the (lookup_type cache' typ c) RS
+            Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
         |> Thm.adjust_maxidx_thm ~1);
   in (ths, cache') end;