# 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