# HG changeset patch
# User bulwahn
# Date 1269876655 -7200
# Node ID affb6e1041e1d4b62d61667bb2075ff6feab2fd8
# Parent  385f706eff24ed4be2560db7a3281f36ca288a38
tuned

diff -r 385f706eff24 -r affb6e1041e1 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 29 17:30:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 29 17:30:55 2010 +0200
@@ -31,11 +31,8 @@
   case Item_Net.retrieve net t of
     [] => NONE
   | [(f, p)] =>
-    let
-      val subst = Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)
-    in
-      SOME (Envir.subst_term subst p)
-    end
+    SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p)
+      handle Pattern.MATCH => NONE
   | _ => NONE
 
 fun pred_of_function thy name =