tuned;
authorwenzelm
Thu Mar 06 12:58:51 2014 +0100 (2014-03-06)
changeset 55953b19373bd7ea8
parent 55952 2f85cc6c27d4
child 55954 a29aefc88c8d
tuned;
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:43:29 2014 +0100
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:58:51 2014 +0100
     1.3 @@ -233,12 +233,12 @@
     1.4              (false, Consts.intern (Proof_Context.consts_of ctxt) c);
     1.5          fun get_free x =
     1.6            let
     1.7 -            val skolem = Variable.lookup_fixed ctxt x;
     1.8 +            val fixed = Variable.lookup_fixed ctxt x;
     1.9              val is_const = can (decode_const ctxt) x orelse Long_Name.is_qualified x;
    1.10              val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
    1.11            in
    1.12              if Variable.is_const ctxt x then NONE
    1.13 -            else if is_some skolem then skolem
    1.14 +            else if is_some fixed then fixed
    1.15              else if not is_const orelse is_declared then SOME x
    1.16              else NONE
    1.17            end;