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 \ int) \ nat"