# HG changeset patch
# User wenzelm
# Date 1288382868 -7200
# Node ID 805ce1d64af0e350c44e99891b48f0c0c522454f
# Parent  329cd9dd5949e76036e1b798438a61228ebcb29d
proper signature constraint for ML structure;
explicit theory setup, which is customary outside Pure;
formal @{binding} instead of Binding.name;

diff -r 329cd9dd5949 -r 805ce1d64af0 src/HOL/ex/Coercion_Examples.thy
--- a/src/HOL/ex/Coercion_Examples.thy	Fri Oct 29 21:49:33 2010 +0200
+++ b/src/HOL/ex/Coercion_Examples.thy	Fri Oct 29 22:07:48 2010 +0200
@@ -9,6 +9,8 @@
 uses "~~/src/Tools/subtyping.ML"
 begin
 
+setup Subtyping.setup
+
 (* Coercion/type maps definitions*)
 
 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
diff -r 329cd9dd5949 -r 805ce1d64af0 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Fri Oct 29 21:49:33 2010 +0200
+++ b/src/Tools/subtyping.ML	Fri Oct 29 22:07:48 2010 +0200
@@ -9,9 +9,10 @@
   datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT
   val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
     term list -> term list
+  val setup: theory -> theory
 end;
 
-structure Subtyping =
+structure Subtyping: SUBTYPING =
 struct
 
 (** coercions data **)
@@ -642,24 +643,21 @@
 
 (** installation **)
 
+(* term check *)
+
 fun coercion_infer_types ctxt =
   infer_types ctxt
     (try (Consts.the_constraint (ProofContext.consts_of ctxt)))
     (ProofContext.def_type ctxt);
 
-local
-
-fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
-  let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
-
-in
-
-val _ = add (op aconv) (Syntax.add_term_check ~100 "coercions") coercion_infer_types;
-
-end;
+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);
 
 
-(* interface *)
+(* declarations *)
 
 fun add_type_map map_fun context =
   let
@@ -753,12 +751,16 @@
     map_coes_and_graph coercion_data_update context
   end;
 
-val _ = Context.>> (Context.map_theory
-  (Attrib.setup (Binding.name "coercion") (Scan.lift Parse.term >>
+
+(* theory setup *)
+
+val setup =
+  Context.theory_map add_term_check #>
+  Attrib.setup @{binding coercion} (Scan.lift Parse.term >>
     (fn t => fn (context, thm) => (add_coercion t context, thm)))
     "declaration of new coercions" #>
-  Attrib.setup (Binding.name "map_function") (Scan.lift Parse.term >>
+  Attrib.setup @{binding map_function} (Scan.lift Parse.term >>
     (fn t => fn (context, thm) => (add_type_map t context, thm)))
-    "declaration of new map functions"));
+    "declaration of new map functions";
 
 end;