1.1 --- a/src/HOL/Complex_Main.thy	Wed Dec 01 11:06:01 2010 +0100
     1.2 +++ b/src/HOL/Complex_Main.thy	Wed Dec 01 11:32:24 2010 +0100
     1.3 @@ -10,6 +10,9 @@
     1.4    Ln
     1.5    Taylor
     1.6    Deriv
     1.7 +uses "~~/src/Tools/subtyping.ML"
     1.8  begin
     1.9  
    1.10 +setup Subtyping.setup
    1.11 +
    1.12  end

     2.1 --- a/src/HOL/IsaMakefile	Wed Dec 01 11:06:01 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Dec 01 11:32:24 2010 +0100
     2.3 @@ -385,6 +385,7 @@
     2.4  	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
     2.5  
     2.6  HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
     2.7 +  $(SRC)/Tools/subtyping.ML \
     2.8    Archimedean_Field.thy \
     2.9    Complex.thy \
    2.10    Complex_Main.thy \
    2.11 @@ -408,9 +409,9 @@
    2.12    Series.thy \
    2.13    SupInf.thy \
    2.14    Taylor.thy \
    2.15 -  Transcendental.thy \
    2.16 +  Tools/SMT/smt_real.ML \
    2.17    Tools/float_syntax.ML \
    2.18 -  Tools/SMT/smt_real.ML
    2.19 +  Transcendental.thy
    2.20  
    2.21  $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
    2.22  	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
    2.23 @@ -1049,7 +1050,7 @@
    2.24    ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy	\
    2.25    ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy	\
    2.26    ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML	\
    2.27 -  ex/svc_test.thy $(SRC)/Tools/subtyping.ML
    2.28 +  ex/svc_test.thy
    2.29  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    2.30  
    2.31  

     3.1 --- a/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 11:06:01 2010 +0100
     3.2 +++ b/src/HOL/ex/Coercion_Examples.thy	Wed Dec 01 11:32:24 2010 +0100
     3.3 @@ -5,12 +5,9 @@
     3.4  *)
     3.5  
     3.6  theory Coercion_Examples
     3.7 -imports Main
     3.8 -uses "~~/src/Tools/subtyping.ML"
     3.9 +imports Complex_Main
    3.10  begin
    3.11  
    3.12 -setup Subtyping.setup
    3.13 -
    3.14  (* Error messages test *)
    3.15  
    3.16  consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"