src/HOL/Bali/Name.thy
changeset 35431 8758fe1fc9f8
parent 35315 fbdc860d87a3
child 37956 ee939247b2fb
--- a/src/HOL/Bali/Name.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOL/Bali/Name.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -78,11 +78,7 @@
   qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
 
 translations
-  "mname"  <= "Name.mname"
-  "xname"  <= "Name.xname"
-  "tname"  <= "Name.tname"
-  "ename"  <= "Name.ename"
-  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
+  (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"