# HG changeset patch
# User haftmann
# Date 1390690249 -3600
# Node ID 525309c2e4ee8c5fb2f6edd8d4e831f640204c90
# Parent  2bb3cd36bcf7ade02d9313f61716db7ff632b0b1
more abstract syntax passing

diff -r 2bb3cd36bcf7 -r 525309c2e4ee src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -356,7 +356,7 @@
       (Code_Symbol.dest_class_instance_data printings);
   in
     (names_const @ names_tyco @ names_class @ names_inst,
-      (const_syntax, tyco_syntax, class_syntax))
+      (Symtab.lookup const_syntax, Symtab.lookup tyco_syntax, Symtab.lookup class_syntax))
   end;
 
 fun project_program thy names_hidden names1 program2 =
@@ -392,9 +392,9 @@
       reserved_syms = reserved,
       identifiers = identifiers,
       includes = includes,
-      const_syntax = Symtab.lookup const_syntax,
-      tyco_syntax = Symtab.lookup tyco_syntax,
-      class_syntax = Symtab.lookup class_syntax },
+      const_syntax = const_syntax,
+      tyco_syntax = tyco_syntax,
+      class_syntax = class_syntax },
       program)
   end;