--- a/src/ZF/Tools/induct_tacs.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Thu Oct 15 23:28:10 2009 +0200
@@ -74,7 +74,7 @@
let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
(v, #1 (dest_Const (head_of A)))
| mk_pair _ = raise Match
- val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
+ val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop))
(#2 (OldGoals.strip_context Bi))
in case AList.lookup (op =) pairs var of
NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)