diff -r cbc38731d42f -r 0fbed69ff081 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -169,7 +169,7 @@
           SOME raw_split_thm =>
           let
             val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm
-            val (assms, concl) = Logic.strip_horn (prop_of split_thm)
+            val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
             val (_, [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)
@@ -311,7 +311,7 @@
   let
     fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
     (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
-    val intro_t = Logic.unvarify_global (prop_of intro)
+    val intro_t = Logic.unvarify_global (Thm.prop_of intro)
     val (prems, concl) = Logic.strip_horn intro_t
     val frees = map fst (Term.add_frees intro_t [])
     fun rewrite prem names =