# HG changeset patch
# User wenzelm
# Date 1297195152 -3600
# Node ID 996b0c14a430bbe3b08f877cea2b9f039fb0205f
# Parent  2fb760843e174af651344ec744eddaf654d7cc68
discontinued obsolete alias HOL.thy for @{theory HOL} in ML;

diff -r 2fb760843e17 -r 996b0c14a430 src/HOL/Typedef.thy
--- 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"