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