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