src/Pure/axclass.ML
changeset 17703 6ec36bad47ea
parent 17496 26535df536ae
child 17756 d4a35f82fbb4
--- a/src/Pure/axclass.ML	Thu Sep 29 00:58:55 2005 +0200
+++ b/src/Pure/axclass.ML	Thu Sep 29 00:58:56 2005 +0200
@@ -218,6 +218,7 @@
     (*store info*)
     val final_thy =
       axms_thy
+      |> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT --> propT)]
       |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts))
       |> Theory.restore_naming class_thy
       |> AxclassesData.map (Symtab.update (class, info));