# HG changeset patch
# User wenzelm
# Date 1149257179 -7200
# Node ID c7e9cc10acc852484a472ad1609593e29e6595a1
# Parent  2d0896653e7a28ca25954e277030b100b1bdde87
merge: always normalize (and check!) reductions;

diff -r 2d0896653e7a -r c7e9cc10acc8 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Jun 01 23:53:29 2006 +0200
+++ b/src/Pure/defs.ML	Fri Jun 02 16:06:19 2006 +0200
@@ -149,6 +149,8 @@
     val _ = forall (acyclic pp defs const) (the_default deps deps');
   in deps' end;
 
+in
+
 fun normalize pp =
   let
     fun norm_update (c, {reducts, ...}: def) (changed, defs) =
@@ -168,8 +170,6 @@
       reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
   in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
 
-in
-
 fun dependencies pp (c, args) restr deps =
   map_def c (fn (specs, restricts, reducts) =>
     let
@@ -190,7 +190,10 @@
       else dependencies pp (c, args) restr deps defs;
     fun add_def (c, {restricts, reducts, ...}: def) =
       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
-  in Defs (Symtab.join join_specs (defs1, defs2) |> Symtab.fold add_def defs2) end;
+  in
+    Defs (Symtab.join join_specs (defs1, defs2)
+      |> normalize pp |> Symtab.fold add_def defs2)
+  end;
 
 
 (* define *)