replaced early'' flag by inverted authentic'';
authorwenzelm
Wed May 17 22:34:45 2006 +0200 (2006-05-17)
changeset 196779d54d6d3bc28
parent 19676 187234ec6050
child 19678 d1a15431de34
replaced early'' flag by inverted authentic'';
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Wed May 17 22:34:44 2006 +0200
     1.2 +++ b/src/Pure/consts.ML	Wed May 17 22:34:45 2006 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  type decl =
     1.6    (typ * kind) *
     1.7 -  bool; (*early externing*)
     1.8 +  bool; (*authentic syntax*)
     1.9  
    1.10  datatype T = Consts of
    1.11   {decls: (decl * stamp) NameSpace.table,
    1.12 @@ -61,8 +61,8 @@
    1.13  fun eq_consts (Consts (_, s1), Consts (_, s2)) = s1 = s2;
    1.14  
    1.15  fun make_consts (decls, constraints, rev_abbrevs, expand_abbrevs) =
    1.16 -  Consts ({decls = decls, constraints = constraints,
    1.17 -    expand_abbrevs = expand_abbrevs, rev_abbrevs = rev_abbrevs}, stamp ());
    1.18 +  Consts ({decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs,
    1.19 +    expand_abbrevs = expand_abbrevs}, stamp ());
    1.20  
    1.21  fun map_consts f (Consts ({decls, constraints, rev_abbrevs, expand_abbrevs}, _)) =
    1.22    make_consts (f (decls, constraints, rev_abbrevs, expand_abbrevs));
    1.23 @@ -114,13 +114,13 @@
    1.24  
    1.25  fun extern_early consts c =
    1.26    (case try (the_const consts) c of
    1.27 -    SOME (_, false) => Syntax.constN ^ c
    1.28 +    SOME (_, true) => Syntax.constN ^ c
    1.29    | _ => extern consts c);
    1.30  
    1.31  fun syntax consts (c, mx) =
    1.32    let
    1.33 -    val ((T, _), early) = the_const consts c handle TYPE (msg, _, _) => error msg;
    1.34 -    val c' = if early then NameSpace.base c else Syntax.constN ^ c;
    1.35 +    val ((T, _), authentic) = the_const consts c handle TYPE (msg, _, _) => error msg;
    1.36 +    val c' = if authentic then Syntax.constN ^ c else NameSpace.base c;
    1.37    in (c', T, mx) end;
    1.38  
    1.39  
    1.40 @@ -201,7 +201,7 @@
    1.41  
    1.42  (* declarations *)
    1.43  
    1.44 -fun declare naming ((c, declT), early) =
    1.45 +fun declare naming ((c, declT), authentic) =
    1.46      map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
    1.47    let
    1.48      fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos
    1.49 @@ -209,7 +209,7 @@
    1.50        | args_of (TFree _) _ = I
    1.51      and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is
    1.52        | args_of_list [] _ _ = I;
    1.53 -    val decl = (((declT, LogicalConst (map #2 (rev (args_of declT [] [])))), early), stamp ());
    1.54 +    val decl = (((declT, LogicalConst (map #2 (rev (args_of declT [] [])))), authentic), stamp ());
    1.55    in (extend_decls naming (c, decl) decls, constraints, rev_abbrevs, expand_abbrevs) end);
    1.56  
    1.57  
    1.58 @@ -247,7 +247,7 @@
    1.59  
    1.60  in
    1.61  
    1.62 -fun abbreviate pp tsig naming mode ((c, raw_rhs), early) consts =
    1.63 +fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts =
    1.64    let
    1.65      val rhs = raw_rhs
    1.66        |> Term.map_term_types (Type.cert_typ tsig)
    1.67 @@ -259,7 +259,7 @@
    1.68      consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
    1.69        let
    1.70          val decls' = decls
    1.71 -          |> extend_decls naming (c, (((T, Abbreviation rhs'), early), stamp ()));
    1.72 +          |> extend_decls naming (c, (((T, Abbreviation rhs'), authentic), stamp ()));
    1.73          val rev_abbrevs' = rev_abbrevs
    1.74            |> fold (curry Symtab.update_list mode) (rev_abbrev (NameSpace.full naming c, T) rhs);
    1.75        in (decls', constraints, rev_abbrevs', expand_abbrevs) end)