--- 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;