tuned

--- a/src/HOL/Typerep.thy	Mon Jan 19 13:37:24 2009 +0100
+++ b/src/HOL/Typerep.thy	Wed Jan 21 16:47:01 2009 +0100
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Library/RType.thy
-    ID:         $Id$
+(*  Title:      HOL/Typerep.thy
     Author:     Florian Haftmann, TU Muenchen
 *)
 
@@ -15,9 +14,7 @@
   fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
 begin
 
-definition
-  typerep_of :: "'a \<Rightarrow> typerep"
-where
+definition typerep_of :: "'a \<Rightarrow> typerep" where
   [simp]: "typerep_of x = typerep TYPE('a)"
 
 end