# HG changeset patch
# User haftmann
# Date 1262610597 -3600
# Node ID 5eaff81220a91877e8dfc049d5ec4baea27aa746
# Parent  25bd3ed2ac9f2d4fd4ee751c3f5851ac4a0b970d
dropped redundant name declarations

diff -r 25bd3ed2ac9f -r 5eaff81220a9 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Jan 04 14:09:56 2010 +0100
+++ b/src/Tools/Code/code_ml.ML	Mon Jan 04 14:09:57 2010 +0100
@@ -481,8 +481,6 @@
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
-                  |> intro_base_names
-                      (is_none o syntax_const) deresolve consts
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [