# HG changeset patch
# User wenzelm
# Date 1148161020 -7200
# Node ID 8c03cadf98861d4c125a82fd28c93916e2939e3a
# Parent  a3a8594e19b473e59ab0c5e6a803785d1053b3cf
class axiomatization: finals;

diff -r a3a8594e19b4 -r 8c03cadf9886 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat May 20 23:36:59 2006 +0200
+++ b/src/Pure/axclass.ML	Sat May 20 23:37:00 2006 +0200
@@ -358,6 +358,7 @@
     thy
     |> Sign.primitive_class (bclass, super)
     |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
+    |> Theory.add_finals_i false [Term.head_of (Logic.mk_inclass (Term.aT [], class))]
   end;
 
 in