# HG changeset patch
# User bulwahn
# Date 1270046681 -7200
# Node ID 8103572203886ef394cb403725dd2a18692f5412
# Parent  88203782cf12a40536aa4cb0090c732af9316efd
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler

diff -r 88203782cf12 -r 810357220388 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Mar 31 16:44:41 2010 +0200
@@ -28,12 +28,15 @@
 )
 
 fun lookup thy net t =
-  case Item_Net.retrieve net t of
-    [] => NONE
-  | [(f, p)] =>
+  let
+    val poss_preds = map_filter (fn (f, p) =>
     SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p)
-      handle Pattern.MATCH => NONE
-  | _ => NONE
+    handle Pattern.MATCH => NONE) (Item_Net.retrieve net t)
+  in
+    case poss_preds of
+      [p] => SOME p
+    | _ => NONE
+  end
 
 fun pred_of_function thy name =
   case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of