diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed May 09 07:53:04 2007 +0200
+++ b/src/HOL/Orderings.thy	Wed May 09 07:53:06 2007 +0200
@@ -6,7 +6,7 @@
 header {* Syntactic and abstract orders *}
 
 theory Orderings
-imports HOL
+imports Code_Generator
 begin
 
 subsection {* Order syntax *}
@@ -798,7 +798,7 @@
 
 subsection {* Order on bool *}
 
-instance bool :: linorder 
+instance bool :: order 
   le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
   less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
   by default (auto simp add: le_bool_def less_bool_def)
@@ -892,11 +892,6 @@
 
 ML {*
 val monoI = @{thm monoI};
-
-structure HOL =
-struct
-  val thy = theory "HOL";
-end;
-*}  -- "belongs to theory HOL"
+*}
 
 end