# HG changeset patch # User wenzelm # Date 1148161537 -7200 # Node ID 7706aeac6cf12a7acb414ac7d0233fb75cbe39a6 # Parent 08894a78400bb316efcff2705a9edee6808566e4 made smlnj happy; diff -r 08894a78400b -r 7706aeac6cf1 src/Pure/defs.ML --- a/src/Pure/defs.ML Sat May 20 23:37:04 2006 +0200 +++ b/src/Pure/defs.ML Sat May 20 23:45:37 2006 +0200 @@ -148,7 +148,7 @@ fun normalize_deps prt defs0 (Defs defs) = let fun norm const deps = perhaps (normalize prt defs0 const) deps; - fun norm_update (c, {reducts, ...}) = + fun norm_update (c, {reducts, ...}: def) = let val reducts' = reducts |> map (fn (args, deps) => (args, norm (c, args) deps)) in if reducts = reducts' then I else Symtab.map_entry c (map_def (fn (specs, pattern, restricts, reducts) => @@ -183,7 +183,7 @@ fun add_deps (c, args) pat deps defs = if AList.defined (op =) (reducts_of defs c) args then defs else dependencies (print_const pp) (c, args) pat deps defs; - fun add_def (c, {pattern, restricts, reducts, ...}) = + fun add_def (c, {pattern, restricts, reducts, ...}: def) = fold (fn (args, deps) => add_deps (c, args) (pattern, restricts) deps) reducts; in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end;