src/HOL/Typerep.thy
changeset 31205 98370b26c2ce
parent 31137 cd3aafc1c631
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Typerep.thy	Tue May 19 13:57:51 2009 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Tue May 19 16:54:55 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  imports Plain String
     1.5  begin
     1.6  
     1.7 -datatype typerep = Typerep message_string "typerep list"
     1.8 +datatype typerep = Typerep String.literal "typerep list"
     1.9  
    1.10  class typerep =
    1.11    fixes typerep :: "'a itself \<Rightarrow> typerep"
    1.12 @@ -45,7 +45,7 @@
    1.13      val ty = Type (tyco, map TFree vs);
    1.14      val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    1.15        $ Free ("T", Term.itselfT ty);
    1.16 -    val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
    1.17 +    val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
    1.18        $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
    1.19      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.20    in