returning an more understandable user error message in the values command
authorbulwahn
Mon Mar 29 17:30:50 2010 +0200 (2010-03-29)
changeset 36031199fe16cdaab
parent 36030 1cd962a0b1a6
child 36032 dfd30b5b4e73
returning an more understandable user error message in the values command
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:50 2010 +0200
     1.3 @@ -3165,7 +3165,10 @@
     1.4      val body = subst_bounds (output_frees, body)
     1.5      val T_compr = HOLogic.mk_ptupleT fp Ts
     1.6      val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees)
     1.7 -    val (pred as Const (name, T), all_args) = strip_comb body
     1.8 +    val (pred as Const (name, T), all_args) =
     1.9 +      case strip_comb body of
    1.10 +        (Const (name, T), all_args) => (Const (name, T), all_args)
    1.11 +      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term_global thy head)
    1.12    in
    1.13      if defined_functions compilation thy name then
    1.14        let