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