src/Pure/Isar/method.ML

         val params = Logic.strip_params Bi
                              (* params of subgoal i as string typ pairs *)
         val params = rev(Term.rename_wrt_term Bi params)
                            (* as they are printed: bound variables with *)
                            (* the same name are renamed during printing *)
-        fun types' (a, ~1) = (case assoc (params, a) of
+        fun types' (a, ~1) = (case AList.lookup (op =) params a of
                 NONE => types (a, ~1)
               | some => some)
           | types' xi = types xi;
         fun internal x = is_some (types' (x, ~1));
         val used = Drule.add_used thm (Drule.add_used st []);