
diff -r d9bd6df700a8 -r 48e01d16dd17 src/HOL/ex/Coercion_Examples.thy
--- a/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 11:06:01 2010 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 11:32:24 2010 +0100
@@ -5,12 +5,9 @@
 *)
 
 theory Coercion_Examples
-imports Main
-uses "~~/src/Tools/subtyping.ML"
+imports Complex_Main
 begin
 
-setup Subtyping.setup
-
 (* Error messages test *)
 
 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"




