setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;

--- a/NEWS	Thu Dec 02 21:48:36 2010 +0100
+++ b/NEWS	Fri Dec 03 17:59:13 2010 +0100
@@ -101,29 +101,32 @@
 
 *** HOL ***
 
-* Quickcheck now by default uses exhaustive testing instead of random testing.
-Random testing can be invoked by quickcheck[random],
+* Quickcheck now by default uses exhaustive testing instead of random
+testing.  Random testing can be invoked by quickcheck[random],
 exhaustive testing by quickcheck[exhaustive].
 
-* Quickcheck instantiates polymorphic types with small finite datatypes
-by default. This enables a simple execution mechanism to handle
-quantifiers and function equality over the finite datatypes.   
-
-* Functions can be declared as coercions and type inference will add them
-as necessary upon input of a term. In Complex_Main, real :: nat => real
-and real :: int => real are declared as coercions. A new coercion function
-f is declared like this:
-
-declare [[coercion f]]
+* Quickcheck instantiates polymorphic types with small finite
+datatypes by default. This enables a simple execution mechanism to
+handle quantifiers and function equality over the finite datatypes.
+
+* Functions can be declared as coercions and type inference will add
+them as necessary upon input of a term. In theory Complex_Main,
+real :: nat => real and real :: int => real are declared as
+coercions. A new coercion function f is declared like this:
+
+  declare [[coercion f]]
 
 To lift coercions through type constructors (eg from nat => real to
 nat list => real list), map functions can be declared, e.g.
 
-declare [[coercion_map map]]
-
-Currently coercion inference is activated only in theories including real
-numbers, i.e. descendants of Complex_Main. In other theories it needs to be
-loaded explicitly: uses "~~/src/Tools/subtyping.ML"
+  declare [[coercion_map map]]
+
+Currently coercion inference is activated only in theories including
+real numbers, i.e. descendants of Complex_Main.  This is controlled by
+the configuration option "infer_coercions", e.g. it can be enabled in
+other theories like this:
+
+  declare [[coercion_enabled]]
 
 * Abandoned locales equiv, congruent and congruent2 for equivalence relations.
 INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)).

--- a/src/HOL/HOL.thy	Thu Dec 02 21:48:36 2010 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 03 17:59:13 2010 +0100
@@ -33,9 +33,11 @@
   "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
   ("Tools/type_mapper.ML")
+  "~~/src/Tools/subtyping.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
+setup Subtyping.setup
 
 
 subsection {* Primitive logic *}

--- a/src/HOL/IsaMakefile	Thu Dec 02 21:48:36 2010 +0100
+++ b/src/HOL/IsaMakefile	Fri Dec 03 17:59:13 2010 +0100
@@ -156,6 +156,14 @@
 	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
 
 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
+  $(SRC)/Provers/Arith/cancel_div_mod.ML \
+  $(SRC)/Provers/Arith/cancel_sums.ML \
+  $(SRC)/Provers/Arith/fast_lin_arith.ML \
+  $(SRC)/Provers/order.ML \
+  $(SRC)/Provers/trancl.ML \
+  $(SRC)/Tools/Metis/metis.ML \
+  $(SRC)/Tools/rat.ML \
+  $(SRC)/Tools/subtyping.ML \
   Complete_Lattice.thy \
   Complete_Partial_Order.thy \
   Datatype.thy \
@@ -182,10 +190,7 @@
   SAT.thy \
   Set.thy \
   Sum_Type.thy \
-  Tools/abel_cancel.ML \
-  Tools/arith_data.ML \
-  Tools/async_manager.ML \
-  Tools/cnf_funcs.ML \
+  Tools/Datatype/datatype.ML \
   Tools/Datatype/datatype_abs_proofs.ML \
   Tools/Datatype/datatype_aux.ML \
   Tools/Datatype/datatype_case.ML \
@@ -193,14 +198,12 @@
   Tools/Datatype/datatype_data.ML \
   Tools/Datatype/datatype_prop.ML \
   Tools/Datatype/datatype_realizer.ML \
-  Tools/Datatype/datatype.ML \
-  Tools/dseq.ML \
   Tools/Function/context_tree.ML \
+  Tools/Function/fun.ML \
+  Tools/Function/function.ML \
   Tools/Function/function_common.ML \
   Tools/Function/function_core.ML \
   Tools/Function/function_lib.ML \
-  Tools/Function/function.ML \
-  Tools/Function/fun.ML \
   Tools/Function/induction_schema.ML \
   Tools/Function/lexicographic_order.ML \
   Tools/Function/measure_functions.ML \
@@ -214,17 +217,22 @@
   Tools/Function/size.ML \
   Tools/Function/sum_tree.ML \
   Tools/Function/termination.ML \
-  Tools/inductive_codegen.ML \
-  Tools/inductive.ML \
-  Tools/inductive_realizer.ML \
-  Tools/inductive_set.ML \
-  Tools/lin_arith.ML \
   Tools/Meson/meson.ML \
   Tools/Meson/meson_clausify.ML \
   Tools/Meson/meson_tactic.ML \
   Tools/Metis/metis_reconstruct.ML \
+  Tools/Metis/metis_tactics.ML \
   Tools/Metis/metis_translate.ML \
-  Tools/Metis/metis_tactics.ML \
+  Tools/abel_cancel.ML \
+  Tools/arith_data.ML \
+  Tools/async_manager.ML \
+  Tools/cnf_funcs.ML \
+  Tools/dseq.ML \
+  Tools/inductive.ML \
+  Tools/inductive_codegen.ML \
+  Tools/inductive_realizer.ML \
+  Tools/inductive_set.ML \
+  Tools/lin_arith.ML \
   Tools/nat_arith.ML \
   Tools/primrec.ML \
   Tools/prop_logic.ML \
@@ -237,14 +245,7 @@
   Tools/typedef.ML \
   Transitive_Closure.thy \
   Typedef.thy \
-  Wellfounded.thy \
-  $(SRC)/Provers/Arith/cancel_div_mod.ML \
-  $(SRC)/Provers/Arith/cancel_sums.ML \
-  $(SRC)/Provers/Arith/fast_lin_arith.ML \
-  $(SRC)/Provers/order.ML \
-  $(SRC)/Provers/trancl.ML \
-  $(SRC)/Tools/Metis/metis.ML \
-  $(SRC)/Tools/rat.ML
+  Wellfounded.thy
 
 $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
 	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
@@ -385,7 +386,6 @@
 	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
 
 HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
-  $(SRC)/Tools/subtyping.ML \
   Archimedean_Field.thy \
   Complex.thy \
   Complex_Main.thy \

--- a/src/HOL/RealDef.thy	Thu Dec 02 21:48:36 2010 +0100
+++ b/src/HOL/RealDef.thy	Fri Dec 03 17:59:13 2010 +0100
@@ -9,7 +9,6 @@
 
 theory RealDef
 imports Rat
-uses "~~/src/Tools/subtyping.ML"
 begin
 
 text {*
@@ -1110,8 +1109,7 @@
   real_of_nat_def [code_unfold]: "real == real_of_nat"
   real_of_int_def [code_unfold]: "real == real_of_int"
 
-setup Subtyping.setup
-
+declare [[coercion_enabled]]
 declare [[coercion "real::nat\<Rightarrow>real"]]
 declare [[coercion "real::int\<Rightarrow>real"]]
 

--- a/src/Tools/subtyping.ML	Thu Dec 02 21:48:36 2010 +0100
+++ b/src/Tools/subtyping.ML	Fri Dec 03 17:59:13 2010 +0100
@@ -7,6 +7,7 @@
 signature SUBTYPING =
 sig
   datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT
+  val coercion_enabled: bool Config.T
   val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
     term list -> term list
   val add_type_map: term -> Context.generic -> Context.generic
@@ -716,11 +717,15 @@
     (try (Consts.the_constraint (ProofContext.consts_of ctxt)))
     (ProofContext.def_type ctxt);
 
+val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
+
 val add_term_check =
   Syntax.add_term_check ~100 "coercions"
     (fn xs => fn ctxt =>
-      let val xs' = coercion_infer_types ctxt xs
-      in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end);
+      if Config.get ctxt coercion_enabled then
+        let val xs' = coercion_infer_types ctxt xs
+        in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end
+      else NONE);
 
 
 (* declarations *)
@@ -821,6 +826,7 @@
 (* theory setup *)
 
 val setup =
+  coercion_enabled_setup #>
   Context.theory_map add_term_check #>
   Attrib.setup @{binding coercion}
     (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))