# HG changeset patch
# User wenzelm
# Date 1314025822 -7200
# Node ID 1b1afb1380ee18667f47172d536161efb17e00ca
# Parent  1079ab6b342b1ec58c6ee2b700004576c669a919
old-style numbered structure index is legacy feature (hardly ever used now);

diff -r 1079ab6b342b -r 1b1afb1380ee src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Mon Aug 22 16:12:23 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Aug 22 17:10:22 2011 +0200
@@ -255,8 +255,18 @@
 fun struct_tr structs [Const ("_indexdefault", _)] =
       Syntax.free (the_struct structs 1)
   | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
-      Syntax.free (the_struct structs
-        (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
+      (case Lexicon.read_nat s of
+        SOME n =>
+          let
+            val x = the_struct structs n;
+            val advice =
+              if n = 1 then " -- may be omitted"
+              else " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead";
+            val _ =
+              legacy_feature
+                ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^ advice);
+          in Syntax.free x end
+      | NONE => raise TERM ("struct_tr", [t]))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);