# HG changeset patch
# User haftmann
# Date 1232177359 -3600
# Node ID 941ad06c7f9c4780db8c766de75e24158bcc34ad
# Parent  f83dcdcee6b31440b786e646b5e29d47e1c6acdc
close derivation of classrels

diff -r f83dcdcee6b3 -r 941ad06c7f9c src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Jan 17 08:28:51 2009 +0100
+++ b/src/Pure/axclass.ML	Sat Jan 17 08:29:19 2009 +0100
@@ -295,7 +295,7 @@
   in
     thy
     |> Sign.primitive_classrel (c1, c2)
-    |> put_classrel ((c1, c2), Drule.unconstrainTs th)
+    |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
     |> perhaps complete_arities
   end;