# HG changeset patch # User wenzelm # Date 1140202994 -3600 # Node ID 100bf66d7e85e8b58c9e54957f6852f0fa4a6db9 # Parent fc736dbbe3334c976ab157ade62e467e7519e925 add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints); diff -r fc736dbbe333 -r 100bf66d7e85 src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Feb 17 20:03:10 2006 +0100 +++ b/src/Pure/sign.ML Fri Feb 17 20:03:14 2006 +0100 @@ -27,8 +27,8 @@ val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory val add_abbrevs: bool -> (bstring * string * mixfix) list -> theory -> theory val add_abbrevs_i: bool -> (bstring * term * mixfix) list -> theory -> theory - val add_const_constraint: xstring * string -> theory -> theory - val add_const_constraint_i: string * typ -> theory -> theory + val add_const_constraint: xstring * string option -> theory -> theory + val add_const_constraint_i: string * typ option -> theory -> theory val add_classes: (bstring * xstring list) list -> theory -> theory val add_classes_i: (bstring * class list) list -> theory -> theory val add_classrel: (xstring * xstring) list -> theory -> theory @@ -765,14 +765,14 @@ (* add constraints *) -fun gen_add_constraint int_const prep_typ (raw_c, raw_T) thy = +fun gen_add_constraint int_const prep_typ (raw_c, opt_T) thy = let val c = int_const thy raw_c; - val T = Term.zero_var_indexesT (Term.no_dummyT (prep_typ thy raw_T)) + fun prepT raw_T = + let val T = Type.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T))) + in cert_term thy (Const (c, T)); T end handle TYPE (msg, _, _) => error msg; - val _ = cert_term thy (Const (c, T)) - handle TYPE (msg, _, _) => error msg; - in thy |> map_consts (Consts.constrain (c, T)) end; + in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end; val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort); val add_const_constraint_i = gen_add_constraint (K I) certify_typ;