src/Pure/axclass.ML
changeset 20260 990dbc007ca6
parent 20107 239a0efd38b2
child 20548 8ef25fe585a8
     1.1 --- a/src/Pure/axclass.ML	Sun Jul 30 21:28:51 2006 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Jul 30 21:28:52 2006 +0200
     1.3 @@ -425,7 +425,7 @@
     1.4        sort |> map (fn c =>
     1.5          Goal.finish (the (lookup_type cache' typ c) RS
     1.6            Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c))))
     1.7 -        |> Thm.adjust_maxidx_thm);
     1.8 +        |> Thm.adjust_maxidx_thm ~1);
     1.9    in (ths, cache') end;
    1.10  
    1.11  end;