# HG changeset patch
# User wenzelm
# Date 1148425499 -7200
# Node ID 246afe8852bc23febb0ab418af171481e1dbb9fe
# Parent  08de668266771763c44352260c307ad20eeca8b0
axiomatize class: Theory.add_deps;

diff -r 08de66826677 -r 246afe8852bc src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed May 24 01:04:57 2006 +0200
+++ b/src/Pure/axclass.ML	Wed May 24 01:04:59 2006 +0200
@@ -350,6 +350,9 @@
 fun ax_arity prep =
   axiomatize arityN add_arity (fn thy => prep thy #> Logic.mk_arities);
 
+fun class_const c =
+  (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
+
 fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
   let
     val class = Sign.full_name thy bclass;
@@ -358,7 +361,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))]
+    |> Theory.add_deps "" (class_const class) (map class_const super)
   end;
 
 in