# HG changeset patch
# User wenzelm
# Date 1452775873 -3600
# Node ID 27c63722372247d7424586fab583feda73173a90
# Parent  e089e5b02443bccb3b7d0e91a5f19f262bb02944
tuned;

diff -r e089e5b02443 -r 27c637223722 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Jan 14 12:20:49 2016 +0100
+++ b/src/Pure/defs.ML	Thu Jan 14 13:51:13 2016 +0100
@@ -206,6 +206,10 @@
 
 fun normalize context =
   let
+    fun check_def defs (c, {reducts, ...}: def) =
+      reducts |> forall (fn (args, deps) => forall (wellformed context defs (c, args)) deps);
+    fun check_defs defs = Itemtab.forall (check_def defs) defs;
+
     fun norm_update (c, {reducts, ...}: def) (changed, defs) =
       let
         val reducts' = reducts |> map (fn (args, deps) =>
@@ -214,13 +218,11 @@
         if reducts = reducts' then (changed, defs)
         else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
       end;
-    fun norm_all defs =
+    fun norm_loop defs =
       (case Itemtab.fold norm_update defs (false, defs) of
-        (true, defs') => norm_all defs'
+        (true, defs') => norm_loop defs'
       | (false, _) => defs);
-    fun check defs (c, {reducts, ...}: def) =
-      reducts |> forall (fn (args, deps) => forall (wellformed context defs (c, args)) deps);
-  in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end;
+  in norm_loop #> tap check_defs end;
 
 fun dependencies context (c, args) restr deps =
   map_def c (fn (specs, restricts, reducts) =>