--- a/src/HOL/Tools/inductive_package.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon Sep 12 18:20:32 2005 +0200
@@ -230,7 +230,7 @@
fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
let val f = prod_factors [] u
- in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end
+ in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
| mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
| mg_prod_factors ts (fs, _) = fs;