tuned;

--- a/src/Pure/Syntax/local_syntax.ML	Sat May 25 15:37:53 2013 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Sat May 25 16:55:27 2013 +0200
@@ -61,8 +61,8 @@
 
     val local_syntax = thy_syntax
       |> Syntax.update_trfuns
-          ([], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_parse_translation structs),
-           [], map Syntax_Ext.mk_trfun (Syntax_Trans.struct_print_ast_translation structs))
+          ([], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_tr structs)],
+           [], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_ast_tr' structs)])
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
   in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
 

--- a/src/Pure/Syntax/syntax_trans.ML	Sat May 25 15:37:53 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Sat May 25 16:55:27 2013 +0200
@@ -51,10 +51,8 @@
   val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
   val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
   val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
-  val struct_parse_translation: string list ->
-    (string * (Proof.context -> term list -> term)) list
-  val struct_print_ast_translation: string list ->
-    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
+  val struct_tr: string list -> string * (Proof.context -> term list -> term)
+  val struct_ast_tr': string list -> string * (Proof.context -> Ast.ast list -> Ast.ast)
 end;
 
 structure Syntax_Trans: SYNTAX_TRANS =
@@ -245,12 +243,13 @@
 fun index_tr [t] = t
   | index_tr ts = raise TERM ("index_tr", ts);
 
-fun the_struct [] = error "Illegal reference to implicit structure"
-  | the_struct (x :: _) = x;
-
-fun struct_tr structs [Const ("_indexdefault", _)] =
-      Syntax.const (Lexicon.mark_fixed (the_struct structs))
-  | struct_tr _ ts = raise TERM ("struct_tr", ts);
+fun struct_tr structs =
+  ("_struct", fn _ =>
+    (fn [Const ("_indexdefault", _)] =>
+        (case structs of
+          x :: _ => Syntax.const (Lexicon.mark_fixed x)
+        | _ => error "Illegal reference to implicit structure")
+      | ts => raise TERM ("struct_tr", ts)));
 
 
 
@@ -492,10 +491,13 @@
 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
   | index_ast_tr' _ = raise Match;
 
-fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] =
-      Ast.Appl [Ast.Constant "_free",
-        Ast.Variable (the_struct structs handle ERROR _ => raise Match)]
-  | struct_ast_tr' _ _ = raise Match;
+fun struct_ast_tr' structs =
+  ("_struct", fn _ =>
+    (fn [Ast.Constant "_indexdefault"] =>
+        (case structs of
+          x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
+        | _ => raise Match)
+      | _ => raise Match));
 
 
 
@@ -535,9 +537,6 @@
   ("\\<^const>==>", fn _ => impl_ast_tr'),
   ("_index", fn _ => index_ast_tr')];
 
-fun struct_parse_translation structs = [("_struct", fn _ => struct_tr structs)];
-fun struct_print_ast_translation structs = [("_struct", fn _ => struct_ast_tr' structs)];
-
 end;
 
 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;