src/HOL/Code_Eval.thy
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)