src/Pure/sign.ML
changeset 24959 119793c84647
parent 24949 5f00e3532418
child 24973 dc67846b00c0
     1.1 --- a/src/Pure/sign.ML	Thu Oct 11 15:59:31 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Oct 11 16:05:23 2007 +0200
     1.3 @@ -156,8 +156,7 @@
     1.4    val simple_read_term: theory -> typ -> string -> term
     1.5    val read_term: theory -> string -> term
     1.6    val read_prop: theory -> string -> term
     1.7 -  val add_consts_authentic: Markup.property list ->
     1.8 -    (bstring * typ * mixfix) list -> theory -> theory
     1.9 +  val declare_const: Markup.property list -> (bstring * typ * mixfix) -> theory -> term * theory
    1.10    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.11    val add_abbrev: string -> Markup.property list ->
    1.12      bstring * term -> theory -> (term * term) * theory
    1.13 @@ -657,8 +656,8 @@
    1.14  
    1.15  val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    1.16  val add_modesyntax_i = gen_add_syntax (K I);
    1.17 -val add_syntax = add_modesyntax Syntax.default_mode;
    1.18 -val add_syntax_i = add_modesyntax_i Syntax.default_mode;
    1.19 +val add_syntax = add_modesyntax Syntax.mode_default;
    1.20 +val add_syntax_i = add_modesyntax_i Syntax.mode_default;
    1.21  val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
    1.22  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
    1.23  
    1.24 @@ -675,26 +674,30 @@
    1.25  
    1.26  fun gen_add_consts prep_typ authentic tags raw_args thy =
    1.27    let
    1.28 -    val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    1.29 +    val prepT = Type.no_tvars o Term.no_dummyT o prep_typ thy;
    1.30      fun prep (raw_c, raw_T, raw_mx) =
    1.31        let
    1.32          val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.33 -        val c' = if authentic then Syntax.constN ^ full_name thy c else c;
    1.34 +        val full_c = full_name thy c;
    1.35 +        val c' = if authentic then Syntax.constN ^ full_c else c;
    1.36          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.37            cat_error msg ("in declaration of constant " ^ quote c);
    1.38 -      in ((c, T), (c', T, mx)) end;
    1.39 +        val T' = Compress.typ thy (Logic.varifyT T);
    1.40 +      in ((c, T'), (c', T', mx), Const (full_c, T)) end;
    1.41      val args = map prep raw_args;
    1.42    in
    1.43      thy
    1.44      |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
    1.45      |> add_syntax_i (map #2 args)
    1.46 +    |> pair (map #3 args)
    1.47    end;
    1.48  
    1.49  in
    1.50  
    1.51 -val add_consts = gen_add_consts read_typ false [];
    1.52 -val add_consts_i = gen_add_consts certify_typ false [];
    1.53 -val add_consts_authentic = gen_add_consts certify_typ true;
    1.54 +val add_consts = snd oo gen_add_consts read_typ false [];
    1.55 +val add_consts_i = snd oo gen_add_consts certify_typ false [];
    1.56 +
    1.57 +fun declare_const tags arg = gen_add_consts certify_typ true tags [arg] #>> the_single;
    1.58  
    1.59  end;
    1.60