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