diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Bali/AxExample.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -42,7 +42,7 @@
 
 ML \<open>
 fun inst1_tac ctxt s t xs st =
-  (case AList.lookup (=) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
+  (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
     SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st
   | NONE => Seq.empty);