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