# [isabelle] [BUG?] value not working on an expression resulting in "True"

```Hi all, I'm a software developer and a new Isabelle user, practicing with the
tutorial. I'm using Isabelle 2007.

Note these two lines in the below theory (derived from § 2.5.6 of the
tutorial,
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf):

normal_form "val (Const True)"

gives:

"True"
:: "bool"

While
value "val (Const True)"  (* this fails *)
fails (and there are no variables, so there's no reason for this).

Here's the theory:

theory ExBoolexBugReport imports Main begin
datatype boolex = Const bool | Neg boolex | And boolex boolex

consts
"val" :: "boolex \<Rightarrow> bool"
primrec
"val (Const b) = b"
"val (Neg boolex) = (\<not> (val boolex))"
"val (And b c) = ((val b) \<and> (val c))"

value "True"

normal_form "val (Const True)"
value "val (Const True)" (* this fails *)
value "val (Const (True::bool))"

end

Here's the error I get in the *responses* Emacs buffer.

*** Error: in 'ML', line 11.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
***    \$( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))
***
*** Error: in 'ML', line 11.
*** Can't unify Term.term with EvalTerm.Generated.boolex
***    (Different type constructors) Found near
***    \$( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))
***
*** Error: in 'ML', line 14.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
***    \$( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))
***
*** Error: in 'ML', line 14.
*** Can't unify Term.term with EvalTerm.Generated.boolex
***    (Different type constructors) Found near
***    \$( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))
***
*** Error: in 'ML', line 19.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
***    \$( \$( Const( ...), ...(...)), term_of_boolex(x2))
***
*** Error: in 'ML', line 19.
*** Can't unify Term.term with EvalTerm.Generated.boolex
***    (Different type constructors) Found near
***    \$( \$( Const( ...), ...(...)), term_of_boolex(x2))
***
*** At command "value".

If needed: I'm using ProofGeneral-3.7pre071112 and Emacs 22.1 as provided by
Ubuntu 7.04, in case it makes any difference.