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.
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
authorbulwahn
Wed, 31 Mar 2010 16:44:41 +0200
changeset 36051 810357220388
parent 36050 88203782cf12
child 36052 c240b2a5df90
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle