# HG changeset patch
# User wenzelm
# Date 1127948336 -7200
# Node ID 6ec36bad47ea249ad64b85e7359309397a69a366
# Parent  ea88ddeafabe4e7b4ae9d3aa0dccf0ecb2e6477d
Theory.add_finals_i;

diff -r ea88ddeafabe -r 6ec36bad47ea src/Pure/axclass.ML
--- 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));
diff -r ea88ddeafabe -r 6ec36bad47ea src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Sep 29 00:58:55 2005 +0200
+++ b/src/Pure/pure_thy.ML	Thu Sep 29 00:58:56 2005 +0200
@@ -509,7 +509,8 @@
     [Const ("==", [aT, aT] ---> propT),
      Const ("==>", [propT, propT] ---> propT),
      Const ("all", (aT --> propT) --> propT),
-     Const ("TYPE", a_itselfT)]
+     Const ("TYPE", a_itselfT),
+     Const (Term.dummy_patternN, aT)]
   |> Theory.add_modesyntax ("", false)
     (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   |> Theory.add_trfuns Syntax.pure_trfuns