consts: replaced early'' flag by inverted authentic'';
authorwenzelm
Wed May 17 22:34:49 2006 +0200 (2006-05-17)
changeset 19679ae4c1e2742c1
parent 19678 d1a15431de34
child 19680 6a34b1b1f540
consts: replaced early'' flag by inverted authentic'';
tuned interfaces;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed May 17 22:34:47 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed May 17 22:34:49 2006 +0200
     1.3 @@ -191,9 +191,9 @@
     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: (bstring * typ * mixfix) list -> theory -> theory
     1.8    val add_const_syntax: string * bool -> (string * mixfix) list -> theory -> theory
     1.9 -  val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
    1.10 -  val add_abbrevs: string * bool -> (bstring * term * mixfix) list -> theory -> theory
    1.11 +  val add_abbrevs: string * bool -> ((bstring * mixfix) * term) list -> theory -> theory
    1.12    include SIGN_THEORY
    1.13  end
    1.14  
    1.15 @@ -719,16 +719,16 @@
    1.16  
    1.17  local
    1.18  
    1.19 -fun gen_add_consts prep_typ early raw_args thy =
    1.20 +fun gen_add_consts prep_typ authentic raw_args thy =
    1.21    let
    1.22      val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    1.23      fun prep (raw_c, raw_T, raw_mx) =
    1.24        let
    1.25          val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.26 -        val (c', b) = if early then (c, true) else (Syntax.constN ^ full_name thy c, false);
    1.27 +        val c' = if authentic then Syntax.constN ^ full_name thy c else c;
    1.28          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    1.29            cat_error msg ("in declaration of constant " ^ quote c);
    1.30 -      in (((c, T), b), (c', T, mx)) end;
    1.31 +      in (((c, T), authentic), (c', T, mx)) end;
    1.32      val args = map prep raw_args;
    1.33    in
    1.34      thy
    1.35 @@ -739,16 +739,16 @@
    1.36  
    1.37  in
    1.38  
    1.39 -val add_consts = gen_add_consts (read_typ o no_def_sort) true;
    1.40 -val add_consts_i = gen_add_consts certify_typ true;
    1.41 -val add_consts_authentic = gen_add_consts certify_typ false;
    1.42 +val add_consts = gen_add_consts (read_typ o no_def_sort) false;
    1.43 +val add_consts_i = gen_add_consts certify_typ false;
    1.44 +val add_consts_authentic = gen_add_consts certify_typ true;
    1.45  
    1.46  end;
    1.47  
    1.48  
    1.49  (* add abbreviations *)
    1.50  
    1.51 -fun add_abbrevs (mode, inout) = fold (fn (raw_c, raw_t, raw_mx) => fn thy =>
    1.52 +fun add_abbrevs (mode, inout) = fold (fn ((raw_c, raw_mx), raw_t) => fn thy =>
    1.53    let
    1.54      val prep_tm = Compress.term thy o Logic.varify o no_vars (pp thy) o
    1.55        Term.no_dummy_patterns o cert_term_abbrev thy;
    1.56 @@ -760,7 +760,7 @@
    1.57      val T = Term.fastype_of t;
    1.58    in
    1.59      thy
    1.60 -    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), false))
    1.61 +    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), true))
    1.62      |> map_syn (Syntax.extend_consts [c])
    1.63      |> add_modesyntax_i (mode, inout) [(c', T, mx)]
    1.64    end);