changeset 17314 | 04e21a27c0ad |
parent 17223 | 430edc6b7826 |
child 17412 | e26cb20ef0cc |
--- a/src/ZF/Tools/induct_tacs.ML Thu Sep 08 16:08:50 2005 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Thu Sep 08 16:09:23 2005 +0200 @@ -84,7 +84,7 @@ | mk_pair _ = raise Match val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop)) (#2 (strip_context Bi)) - in case assoc (pairs, var) of + in case AList.lookup (op =) pairs var of NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var) | SOME t => t end;