diff -r 148f6175fa78 -r d2e5df3d1201 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 23 20:50:51 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 23 20:52:04 2004 +0200
@@ -309,6 +309,21 @@
   else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
 
 
+(* parse translations *)
+
+fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
+
+fun index_tr struct_ (Const ("_noindex", _)) = Syntax.free (struct_ 1)
+  | index_tr struct_ (t as (Const ("_index", _) $ Const (s, _))) =
+      Syntax.free (struct_
+        (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t])))
+  | index_tr _ (Const ("_indexlogic", _) $ t) = t
+  | index_tr _ t = raise TERM ("index_tr", [t]);
+
+fun struct_tr structs [idx] = index_tr (the_struct structs) idx
+  | struct_tr _ ts = raise TERM ("struct_tr", ts);
+
+
 (* print (ast) translations *)
 
 fun index_tr' 1 = Syntax.const "_noindex"
@@ -341,19 +356,6 @@
   | struct_ast_tr' _ _ = raise Match;
 
 
-(* parse translations *)
-
-fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
-
-fun index_tr (Const ("_noindex", _)) = 1
-  | index_tr (t as (Const ("_index", _) $ Const (s, _))) =
-      (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t]))
-  | index_tr t = raise TERM ("index_tr", [t]);
-
-fun struct_tr structs (idx :: ts) = Syntax.free (the_struct structs (index_tr idx))
-  | struct_tr _ ts = raise TERM ("struct_tr", ts);
-
-
 (* add syntax *)
 
 fun mixfix_type mx = replicate (Syntax.mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;