src/Pure/defs.ML
changeset 19695 7706aeac6cf1
parent 19692 bad13b32c0f3
child 19697 423af2e013b8
     1.1 --- a/src/Pure/defs.ML	Sat May 20 23:37:04 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Sat May 20 23:45:37 2006 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4  fun normalize_deps prt defs0 (Defs defs) =
     1.5    let
     1.6      fun norm const deps = perhaps (normalize prt defs0 const) deps;
     1.7 -    fun norm_update (c, {reducts, ...}) =
     1.8 +    fun norm_update (c, {reducts, ...}: def) =
     1.9        let val reducts' = reducts |> map (fn (args, deps) => (args, norm (c, args) deps)) in
    1.10          if reducts = reducts' then I
    1.11          else Symtab.map_entry c (map_def (fn (specs, pattern, restricts, reducts) =>
    1.12 @@ -183,7 +183,7 @@
    1.13      fun add_deps (c, args) pat deps defs =
    1.14        if AList.defined (op =) (reducts_of defs c) args then defs
    1.15        else dependencies (print_const pp) (c, args) pat deps defs;
    1.16 -    fun add_def (c, {pattern, restricts, reducts, ...}) =
    1.17 +    fun add_def (c, {pattern, restricts, reducts, ...}: def) =
    1.18        fold (fn (args, deps) => add_deps (c, args) (pattern, restricts) deps) reducts;
    1.19    in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end;
    1.20