src/HOL/Typerep.thy
changeset 31048 ac146fc38b51
parent 31031 cbec39ebf8f2
child 31137 cd3aafc1c631
     1.1 --- a/src/HOL/Typerep.thy	Wed May 06 16:01:05 2009 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Wed May 06 16:01:06 2009 +0200
     1.3 @@ -1,11 +1,9 @@
     1.4 -(*  Title:      HOL/Typerep.thy
     1.5 -    Author:     Florian Haftmann, TU Muenchen
     1.6 -*)
     1.7 +(* Author: Florian Haftmann, TU Muenchen *)
     1.8  
     1.9  header {* Reflecting Pure types into HOL *}
    1.10  
    1.11  theory Typerep
    1.12 -imports Plain List Code_Message
    1.13 +imports Plain String
    1.14  begin
    1.15  
    1.16  datatype typerep = Typerep message_string "typerep list"
    1.17 @@ -42,7 +40,7 @@
    1.18  struct
    1.19  
    1.20  fun mk f (Type (tyco, tys)) =
    1.21 -      @{term Typerep} $ Message_String.mk tyco
    1.22 +      @{term Typerep} $ HOLogic.mk_message_string tyco
    1.23          $ HOLogic.mk_list @{typ typerep} (map (mk f) tys)
    1.24    | mk f (TFree v) =
    1.25        f v;