--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Sep 30 11:52:22 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Sep 30 15:37:11 2010 +0200
@@ -185,8 +185,9 @@
val (f, args) = strip_comb t
val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
- val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
- val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
+ val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val t' = case_betapply thy t
+ val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
fun flatten_of_assm assm =
let
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))