diff -r 5897b2688ccc -r 41d604e59e93 src/HOL/Code_Eval.thy --- a/src/HOL/Code_Eval.thy Wed Jan 21 16:47:01 2009 +0100 +++ b/src/HOL/Code_Eval.thy Wed Jan 21 16:47:02 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Code_Eval.thy - ID: $Id$ Author: Florian Haftmann, TU Muenchen *) @@ -24,7 +23,7 @@ code_datatype Const App class term_of = typerep + - fixes term_of :: "'a \ term" + fixes term_of :: "'a::{} \ term" lemma term_of_anything: "term_of x \ t" by (rule eq_reflection) (cases "term_of x", cases t, simp)