# HG changeset patch
# User bulwahn
# Date 1269876650 -7200
# Node ID 199fe16cdaab9c4ac70872477ac219f920e99f31
# Parent  1cd962a0b1a69833bba6bda309c8c5bde07c72dd
returning an more understandable user error message in the values command

diff -r 1cd962a0b1a6 -r 199fe16cdaab src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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