src/ZF/Tools/induct_tacs.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4    let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
     1.5               (v, #1 (dest_Const (head_of A)))
     1.6          | mk_pair _ = raise Match
     1.7 -      val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
     1.8 +      val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
     1.9            (#2 (strip_context Bi))
    1.10    in case assoc (pairs, var) of
    1.11         NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
    1.12 @@ -178,7 +178,7 @@
    1.13                (Symtab.update
    1.14                 ((big_rec_name, dt_info), DatatypesData.get thy))
    1.15            |> ConstructorsData.put
    1.16 -               (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
    1.17 +               (Library.foldr Symtab.update (con_pairs, ConstructorsData.get thy))
    1.18            |> Theory.parent_path
    1.19    end;
    1.20