# HG changeset patch
# User wenzelm
# Date 1192288601 -7200
# Node ID fac2ceba75b4be973ff39f5ebfb9260aca99eb82
# Parent  e82ab4962f806f84379d1ae082ab7d5b475c01dc
replaced obsolete Theory.add_finals_i by Theory.add_deps;

diff -r e82ab4962f80 -r fac2ceba75b4 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sat Oct 13 17:16:40 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Sat Oct 13 17:16:41 2007 +0200
@@ -69,7 +69,7 @@
   let val c = Sign.full_name thy (Syntax.const_name bname mx) in
     thy
     |> add_consts [(bname, T, mx)]
-    |> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy')
+    |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
     |> ObjectLogicData.map (new_judgment c)
   end;
 
diff -r e82ab4962f80 -r fac2ceba75b4 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Oct 13 17:16:40 2007 +0200
+++ b/src/Pure/pure_thy.ML	Sat Oct 13 17:16:41 2007 +0200
@@ -580,12 +580,11 @@
     ("prop", typ "prop => prop", NoSyn),
     ("TYPE", typ "'a itself", NoSyn),
     (Term.dummy_patternN, typ "'a", Delimfix "'_")]
-  |> Theory.add_finals_i false
-    [Const ("==", typ "'a => 'a => prop"),
-     Const ("==>", typ "prop => prop => prop"),
-     Const ("all", typ "('a => prop) => prop"),
-     Const ("TYPE", typ "'a itself"),
-     Const (Term.dummy_patternN, typ "'a")]
+  |> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
+  |> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
+  |> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
+  |> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
+  |> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
   |> Sign.add_trfuns Syntax.pure_trfuns
   |> Sign.add_trfunsT Syntax.pure_trfunsT
   |> Sign.local_path