Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
using mode_eq instead of op = for lookup in the predicate compiler
authorbulwahn
Mon, 25 Oct 2010 21:17:15 +0200
changeset 40140 8282b87f957c
parent 40139 6a53d57fa902
child 40141 0e8a4e27a685
using mode_eq instead of op = for lookup in the predicate compiler
src/HOL/Tools/Predicate_Compile/core_data.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle