--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:50 2010 +0200
@@ -3165,7 +3165,10 @@
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