# HG changeset patch # User wenzelm # Date 1288383567 -7200 # Node ID c9acf88447e6970b9544ab8cd8eec6bcdfce3bed # Parent 805ce1d64af0e350c44e99891b48f0c0c522454f export declarations by default, to allow other ML packages by-pass concrete syntax; proper Args parsing for attribute syntax (required for proper treatment of morphisms when declarations are moved between contexts); tuned; diff -r 805ce1d64af0 -r c9acf88447e6 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Fri Oct 29 22:07:48 2010 +0200 +++ b/src/Tools/subtyping.ML Fri Oct 29 22:19:27 2010 +0200 @@ -9,6 +9,8 @@ datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> term list -> term list + val add_type_map: term -> Context.generic -> Context.generic + val add_coercion: term -> Context.generic -> Context.generic val setup: theory -> theory end; @@ -659,10 +661,10 @@ (* declarations *) -fun add_type_map map_fun context = +fun add_type_map raw_t context = let val ctxt = Context.proof_of context; - val t = singleton (Variable.polymorphic ctxt) (Syntax.read_term ctxt map_fun); + val t = singleton (Variable.polymorphic ctxt) raw_t; fun err_str () = "\n\nthe general type signature for a map function is" ^ "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [x1, ..., xn]" ^ @@ -699,10 +701,10 @@ map_tmaps (Symtab.update (snd res, (t, res_av))) context end; -fun add_coercion coercion context = +fun add_coercion raw_t context = let val ctxt = Context.proof_of context; - val t = singleton (Variable.polymorphic ctxt) (Syntax.read_term ctxt coercion); + val t = singleton (Variable.polymorphic ctxt) raw_t; fun err_coercion () = error ("Bad type for coercion " ^ Syntax.string_of_term ctxt t ^ ":\n" ^ @@ -756,11 +758,11 @@ 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))) + Attrib.setup @{binding coercion} + (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t)))) "declaration of new coercions" #> - Attrib.setup @{binding map_function} (Scan.lift Parse.term >> - (fn t => fn (context, thm) => (add_type_map t context, thm))) + Attrib.setup @{binding map_function} + (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t)))) "declaration of new map functions"; end;