src/Pure/defs.ML
changeset 19760 c7e9cc10acc8
parent 19729 cb9e2f0c7658
child 19806 f860b7a98445
     1.1 --- a/src/Pure/defs.ML	Thu Jun 01 23:53:29 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Fri Jun 02 16:06:19 2006 +0200
     1.3 @@ -149,6 +149,8 @@
     1.4      val _ = forall (acyclic pp defs const) (the_default deps deps');
     1.5    in deps' end;
     1.6  
     1.7 +in
     1.8 +
     1.9  fun normalize pp =
    1.10    let
    1.11      fun norm_update (c, {reducts, ...}: def) (changed, defs) =
    1.12 @@ -168,8 +170,6 @@
    1.13        reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
    1.14    in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
    1.15  
    1.16 -in
    1.17 -
    1.18  fun dependencies pp (c, args) restr deps =
    1.19    map_def c (fn (specs, restricts, reducts) =>
    1.20      let
    1.21 @@ -190,7 +190,10 @@
    1.22        else dependencies pp (c, args) restr deps defs;
    1.23      fun add_def (c, {restricts, reducts, ...}: def) =
    1.24        fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
    1.25 -  in Defs (Symtab.join join_specs (defs1, defs2) |> Symtab.fold add_def defs2) end;
    1.26 +  in
    1.27 +    Defs (Symtab.join join_specs (defs1, defs2)
    1.28 +      |> normalize pp |> Symtab.fold add_def defs2)
    1.29 +  end;
    1.30  
    1.31  
    1.32  (* define *)