replaced obsolete Theory.add_finals_i by Theory.add_deps;
authorwenzelm
Sat Oct 13 17:16:41 2007 +0200 (2007-10-13)
changeset 25018fac2ceba75b4
parent 25017 e82ab4962f80
child 25019 3b2d3b8fc7b6
replaced obsolete Theory.add_finals_i by Theory.add_deps;
src/Pure/Isar/object_logic.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/object_logic.ML	Sat Oct 13 17:16:40 2007 +0200
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Oct 13 17:16:41 2007 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4    let val c = Sign.full_name thy (Syntax.const_name bname mx) in
     1.5      thy
     1.6      |> add_consts [(bname, T, mx)]
     1.7 -    |> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy')
     1.8 +    |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
     1.9      |> ObjectLogicData.map (new_judgment c)
    1.10    end;
    1.11  
     2.1 --- a/src/Pure/pure_thy.ML	Sat Oct 13 17:16:40 2007 +0200
     2.2 +++ b/src/Pure/pure_thy.ML	Sat Oct 13 17:16:41 2007 +0200
     2.3 @@ -580,12 +580,11 @@
     2.4      ("prop", typ "prop => prop", NoSyn),
     2.5      ("TYPE", typ "'a itself", NoSyn),
     2.6      (Term.dummy_patternN, typ "'a", Delimfix "'_")]
     2.7 -  |> Theory.add_finals_i false
     2.8 -    [Const ("==", typ "'a => 'a => prop"),
     2.9 -     Const ("==>", typ "prop => prop => prop"),
    2.10 -     Const ("all", typ "('a => prop) => prop"),
    2.11 -     Const ("TYPE", typ "'a itself"),
    2.12 -     Const (Term.dummy_patternN, typ "'a")]
    2.13 +  |> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
    2.14 +  |> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
    2.15 +  |> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
    2.16 +  |> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
    2.17 +  |> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
    2.18    |> Sign.add_trfuns Syntax.pure_trfuns
    2.19    |> Sign.add_trfunsT Syntax.pure_trfunsT
    2.20    |> Sign.local_path