special treatment of structure index 1 in Pure, including legacy warning;
authorwenzelm
Mon Aug 22 23:39:05 2011 +0200 (2011-08-22)
changeset 444339fbee4aab115
parent 44432 61fa3dd485b3
child 44434 3b9b684bfa6f
special treatment of structure index 1 in Pure, including legacy warning;
src/HOL/Groups.thy
src/Pure/Syntax/syntax_trans.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Groups.thy	Tue Aug 23 19:49:21 2011 +0200
     1.2 +++ b/src/HOL/Groups.thy	Mon Aug 22 23:39:05 2011 +0200
     1.3 @@ -103,11 +103,6 @@
     1.4  
     1.5  hide_const (open) zero one
     1.6  
     1.7 -syntax
     1.8 -  "_index1"  :: index    ("\<^sub>1")
     1.9 -translations
    1.10 -  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    1.11 -
    1.12  lemma Let_0 [simp]: "Let 0 f = f 0"
    1.13    unfolding Let_def ..
    1.14  
     2.1 --- a/src/Pure/Syntax/syntax_trans.ML	Tue Aug 23 19:49:21 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Mon Aug 22 23:39:05 2011 +0200
     2.3 @@ -252,21 +252,22 @@
     2.4    if 1 <= i andalso i <= length structs then nth structs (i - 1)
     2.5    else error ("Illegal reference to implicit structure #" ^ string_of_int i);
     2.6  
     2.7 -fun struct_tr structs [Const ("_indexdefault", _)] =
     2.8 -      Syntax.free (the_struct structs 1)
     2.9 +fun legacy_struct structs i =
    2.10 +  let
    2.11 +    val x = the_struct structs i;
    2.12 +    val _ =
    2.13 +      legacy_feature
    2.14 +        ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^
    2.15 +          Position.str_of (Position.thread_data ()) ^
    2.16 +          " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
    2.17 +          (if i = 1 then " (may be omitted)" else ""))
    2.18 +  in x end;
    2.19 +
    2.20 +fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1)
    2.21 +  | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1)
    2.22    | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
    2.23        (case Lexicon.read_nat s of
    2.24 -        SOME n =>
    2.25 -          let
    2.26 -            val x = the_struct structs n;
    2.27 -            val advice =
    2.28 -              " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
    2.29 -              (if n = 1 then " (may be omitted)" else "");
    2.30 -            val _ =
    2.31 -              legacy_feature
    2.32 -                ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^
    2.33 -                  Position.str_of (Position.thread_data ()) ^ advice);
    2.34 -          in Syntax.free x end
    2.35 +        SOME i => Syntax.free (legacy_struct structs i)
    2.36        | NONE => raise TERM ("struct_tr", [t]))
    2.37    | struct_tr _ ts = raise TERM ("struct_tr", ts);
    2.38  
     3.1 --- a/src/Pure/pure_thy.ML	Tue Aug 23 19:49:21 2011 +0200
     3.2 +++ b/src/Pure/pure_thy.ML	Mon Aug 22 23:39:05 2011 +0200
     3.3 @@ -127,6 +127,7 @@
     3.4      ("_strip_positions", typ "'a", NoSyn),
     3.5      ("_constify",   typ "num => num_const",            Delimfix "_"),
     3.6      ("_constify",   typ "float_token => float_const",  Delimfix "_"),
     3.7 +    ("_index1",     typ "index",                       Delimfix "\\<^sub>1"),
     3.8      ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     3.9      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    3.10      ("_indexdefault", typ "index",                     Delimfix ""),