discontinued obsolete alias HOL.thy for @{theory HOL} in ML;

--- a/src/HOL/Typedef.thy	Tue Feb 08 19:57:11 2011 +0100
+++ b/src/HOL/Typedef.thy	Tue Feb 08 20:59:12 2011 +0100
@@ -9,10 +9,6 @@
 uses ("Tools/typedef.ML")
 begin
 
-ML {*
-structure HOL = struct val thy = @{theory HOL} end;
-*}  -- "belongs to theory HOL"
-
 locale type_definition =
   fixes Rep and Abs and A
   assumes Rep: "Rep x \<in> A"