src/HOL/Typedef.thy
changeset 37863 7f113caabcf4
parent 31723 f5cafe803b55
child 38393 7c045c03598f
     1.1 --- a/src/HOL/Typedef.thy	Tue Jul 20 22:03:37 2010 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Tue Jul 20 23:09:49 2010 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  begin
     1.5  
     1.6  ML {*
     1.7 -structure HOL = struct val thy = theory "HOL" end;
     1.8 +structure HOL = struct val thy = @{theory HOL} end;
     1.9  *}  -- "belongs to theory HOL"
    1.10  
    1.11  locale type_definition =