src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
     val output_frees = map2 (curry Free) output_names (rev Ts)
     val body = subst_bounds (output_frees, body)
     val T_compr = HOLogic.mk_ptupleT fp Ts
     val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees)
-    val (pred as Const (name, T), all_args) = strip_comb body
+    val (pred as Const (name, T), all_args) =
+      case strip_comb body of
+        (Const (name, T), all_args) => (Const (name, T), all_args)
+      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term_global thy head)
   in
     if defined_functions compilation thy name then
       let
         fun extract_mode (Const ("Pair", _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
           | extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input