--- 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 ..
--- 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);
--- 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 ""),