close derivation of classrels
authorhaftmann
Sat, 17 Jan 2009 08:29:19 +0100
changeset 29524 941ad06c7f9c
parent 29523 f83dcdcee6b3
child 29525 ad7991d7b5bb
close derivation of classrels
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;