# HG changeset patch
# User wenzelm
# Date 1394107131 -3600
# Node ID b19373bd7ea85f7f8937ad1101c688b52620d353
# Parent  2f85cc6c27d45f1bc463938edb8f648f54bb16ca
tuned;

diff -r 2f85cc6c27d4 -r b19373bd7ea8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:43:29 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:58:51 2014 +0100
@@ -233,12 +233,12 @@
             (false, Consts.intern (Proof_Context.consts_of ctxt) c);
         fun get_free x =
           let
-            val skolem = Variable.lookup_fixed ctxt x;
+            val fixed = Variable.lookup_fixed ctxt x;
             val is_const = can (decode_const ctxt) x orelse Long_Name.is_qualified x;
             val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
           in
             if Variable.is_const ctxt x then NONE
-            else if is_some skolem then skolem
+            else if is_some fixed then fixed
             else if not is_const orelse is_declared then SOME x
             else NONE
           end;