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