src/Pure/sign.ML
changeset 19099 100bf66d7e85
parent 19054 af7cc6063285
child 19244 1d7e51d9828b
     1.1 --- a/src/Pure/sign.ML	Fri Feb 17 20:03:10 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Feb 17 20:03:14 2006 +0100
     1.3 @@ -27,8 +27,8 @@
     1.4    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.5    val add_abbrevs: bool -> (bstring * string * mixfix) list -> theory -> theory
     1.6    val add_abbrevs_i: bool -> (bstring * term * mixfix) list -> theory -> theory
     1.7 -  val add_const_constraint: xstring * string -> theory -> theory
     1.8 -  val add_const_constraint_i: string * typ -> theory -> theory
     1.9 +  val add_const_constraint: xstring * string option -> theory -> theory
    1.10 +  val add_const_constraint_i: string * typ option -> theory -> theory
    1.11    val add_classes: (bstring * xstring list) list -> theory -> theory
    1.12    val add_classes_i: (bstring * class list) list -> theory -> theory
    1.13    val add_classrel: (xstring * xstring) list -> theory -> theory
    1.14 @@ -765,14 +765,14 @@
    1.15  
    1.16  (* add constraints *)
    1.17  
    1.18 -fun gen_add_constraint int_const prep_typ (raw_c, raw_T) thy =
    1.19 +fun gen_add_constraint int_const prep_typ (raw_c, opt_T) thy =
    1.20    let
    1.21      val c = int_const thy raw_c;
    1.22 -    val T = Term.zero_var_indexesT (Term.no_dummyT (prep_typ thy raw_T))
    1.23 +    fun prepT raw_T =
    1.24 +      let val T = Type.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T)))
    1.25 +      in cert_term thy (Const (c, T)); T end
    1.26        handle TYPE (msg, _, _) => error msg;
    1.27 -    val _ = cert_term thy (Const (c, T))
    1.28 -      handle TYPE (msg, _, _) => error msg;
    1.29 -  in thy |> map_consts (Consts.constrain (c, T)) end;
    1.30 +  in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;
    1.31  
    1.32  val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
    1.33  val add_const_constraint_i = gen_add_constraint (K I) certify_typ;