--- 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 =