# HG changeset patch
# User haftmann
# Date 1256215439 -7200
# Node ID 1cefea81ec4f79b667b6993435d63f62187c1e45
# Parent  ba7ff3f9527a11c435917beba23341b610867961
explicit close_derivation

diff -r ba7ff3f9527a -r 1cefea81ec4f src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Oct 22 14:08:01 2009 +0200
+++ b/src/Pure/axclass.ML	Thu Oct 22 14:43:59 2009 +0200
@@ -364,12 +364,11 @@
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
       |> (map o apsnd o map_atyps) (K T);
     val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
-    val th' = Drule.unconstrainTs th;
   in
     thy
     |> fold (snd oo declare_overloaded) missing_params
     |> Sign.primitive_arity (t, Ss, [c])
-    |> put_arity ((t, Ss, c), th')
+    |> put_arity ((t, Ss, c), Thm.close_derivation (Drule.unconstrainTs th))
   end;