diff -r df2862dc23a8 -r 8758fe1fc9f8 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/Representable.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -49,7 +49,7 @@
 text "A TypeRep is an algebraic deflation over the universe of values."
 
 types TypeRep = "udom alg_defl"
-translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
+translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
 
 definition
   Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
@@ -59,7 +59,7 @@
       (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
 
 syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
-translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
+translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
 
 lemma cast_REP:
   "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"