# HG changeset patch
# User bulwahn
# Date 1288034235 -7200
# Node ID 8282b87f957c69c45fc2df62d6ca62ebec9fd968
# Parent  6a53d57fa90276b60c4584aad350b0ba6b1c0746
using mode_eq instead of op = for lookup in the predicate compiler

diff -r 6a53d57fa902 -r 8282b87f957c src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Oct 25 21:17:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Oct 25 21:17:15 2010 +0200
@@ -186,7 +186,7 @@
 
 fun lookup_predfun_data ctxt name mode =
   Option.map rep_predfun_data
-    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
+    (AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode)
 
 fun the_predfun_data ctxt name mode =
   case lookup_predfun_data ctxt name mode of