# HG changeset patch
# User wenzelm
# Date 1365506640 -7200
# Node ID 4ce2f7607d3dcecee0328a07a6ba8f5ca2bbb698
# Parent  28d6eb23522caa451ef99d2d93dfcc569df017ef
more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;

diff -r 28d6eb23522c -r 4ce2f7607d3d src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Apr 09 13:20:09 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Apr 09 13:24:00 2013 +0200
@@ -250,7 +250,8 @@
 fun the_struct [] = error "Illegal reference to implicit structure"
   | the_struct (x :: _) = x;
 
-fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs)
+fun struct_tr structs [Const ("_indexdefault", _)] =
+      Syntax.const (Lexicon.mark_fixed (the_struct structs))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);