changeset 29575 | 41d604e59e93 |
parent 28965 | 1de908189869 |
child 30427 | dfd31c1db060 |
--- 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 \<Rightarrow> term" + fixes term_of :: "'a::{} \<Rightarrow> term" lemma term_of_anything: "term_of x \<equiv> t" by (rule eq_reflection) (cases "term_of x", cases t, simp)