src/HOL/Tools/inductive_package.ML
changeset 17325 d9d50222808e
parent 17261 193b84a70ca4
child 17412 e26cb20ef0cc
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Sep 12 17:29:07 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 12 18:20:32 2005 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4  
     1.5  fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
     1.6          let val f = prod_factors [] u
     1.7 -        in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end
     1.8 +        in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
     1.9        else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
    1.10    | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
    1.11    | mg_prod_factors ts (fs, _) = fs;