made smlnj happy;
authorwenzelm
Sat, 20 May 2006 23:45:37 +0200
changeset 19695 7706aeac6cf1
parent 19694 08894a78400b
child 19696 26a268c299d8
made smlnj happy;
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;