# HG changeset patch
# User wenzelm
# Date 1314049145 -7200
# Node ID 9fbee4aab115f806e20b631eec09e88d02a8f229
# Parent  61fa3dd485b3d57c771f23ceb7d13fe920311cd6
special treatment of structure index 1 in Pure, including legacy warning;

diff -r 61fa3dd485b3 -r 9fbee4aab115 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue Aug 23 19:49:21 2011 +0200
+++ b/src/HOL/Groups.thy	Mon Aug 22 23:39:05 2011 +0200
@@ -103,11 +103,6 @@
 
 hide_const (open) zero one
 
-syntax
-  "_index1"  :: index    ("\<^sub>1")
-translations
-  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
 lemma Let_0 [simp]: "Let 0 f = f 0"
   unfolding Let_def ..
 
diff -r 61fa3dd485b3 -r 9fbee4aab115 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Aug 23 19:49:21 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Aug 22 23:39:05 2011 +0200
@@ -252,21 +252,22 @@
   if 1 <= i andalso i <= length structs then nth structs (i - 1)
   else error ("Illegal reference to implicit structure #" ^ string_of_int i);
 
-fun struct_tr structs [Const ("_indexdefault", _)] =
-      Syntax.free (the_struct structs 1)
+fun legacy_struct structs i =
+  let
+    val x = the_struct structs i;
+    val _ =
+      legacy_feature
+        ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^
+          Position.str_of (Position.thread_data ()) ^
+          " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
+          (if i = 1 then " (may be omitted)" else ""))
+  in x end;
+
+fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1)
+  | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1)
   | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
       (case Lexicon.read_nat s of
-        SOME n =>
-          let
-            val x = the_struct structs n;
-            val advice =
-              " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
-              (if n = 1 then " (may be omitted)" else "");
-            val _ =
-              legacy_feature
-                ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^
-                  Position.str_of (Position.thread_data ()) ^ advice);
-          in Syntax.free x end
+        SOME i => Syntax.free (legacy_struct structs i)
       | NONE => raise TERM ("struct_tr", [t]))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
diff -r 61fa3dd485b3 -r 9fbee4aab115 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Aug 23 19:49:21 2011 +0200
+++ b/src/Pure/pure_thy.ML	Mon Aug 22 23:39:05 2011 +0200
@@ -127,6 +127,7 @@
     ("_strip_positions", typ "'a", NoSyn),
     ("_constify",   typ "num => num_const",            Delimfix "_"),
     ("_constify",   typ "float_token => float_const",  Delimfix "_"),
+    ("_index1",     typ "index",                       Delimfix "\\<^sub>1"),
     ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),