src/HOL/Tools/inductive_realizer.ML
changeset 17325 d9d50222808e
parent 16861 7446b4be013b
child 17485 c39871c52977
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Sep 12 18:20:32 2005 +0200
@@ -275,7 +275,7 @@
     val _ $ (_ $ _ $ S) = concl_of r;
     val (Const (s, _), _) = strip_comb S;
     val rs = getOpt (assoc (rss, s), []);
-  in overwrite (rss, (s, rs @ [r])) end;
+  in AList.update (op =) (s, rs @ [r]) rss end;
 
 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   let