1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 17:44:06 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 17:58:45 2011 +0200
     1.3 @@ -63,8 +63,6 @@
     1.4    val cert_typ: Proof.context -> typ -> typ
     1.5    val cert_typ_syntax: Proof.context -> typ -> typ
     1.6    val cert_typ_abbrev: Proof.context -> typ -> typ
     1.7 -  val get_skolem: Proof.context -> string -> string
     1.8 -  val revert_skolem: Proof.context -> string -> string
     1.9    val infer_type: Proof.context -> string * typ -> typ
    1.10    val inferred_param: string -> Proof.context -> typ * Proof.context
    1.11    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
    1.12 @@ -408,10 +406,7 @@
    1.13  
    1.14  (** prepare variables **)
    1.15  
    1.16 -(* internalize Skolem constants *)
    1.17 -
    1.18 -val lookup_skolem = AList.lookup (op =) o Variable.fixes_of;
    1.19 -fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x);
    1.20 +(* check Skolem constants *)
    1.21  
    1.22  fun no_skolem internal x =
    1.23    if can Name.dest_skolem x then
    1.24 @@ -421,14 +416,6 @@
    1.25    else x;
    1.26  
    1.27  
    1.28 -(* revert Skolem constants -- if possible *)
    1.29 -
    1.30 -fun revert_skolem ctxt x =
    1.31 -  (case find_first (fn (_, y) => y = x) (Variable.fixes_of ctxt) of
    1.32 -    SOME (x', _) => if lookup_skolem ctxt x' = SOME x then x' else x
    1.33 -  | NONE => x);
    1.34 -
    1.35 -
    1.36  
    1.37  (** prepare terms and propositions **)
    1.38  
    1.39 @@ -443,7 +430,7 @@
    1.40  
    1.41  fun inferred_fixes ctxt =
    1.42    let
    1.43 -    val xs = rev (map #2 (Variable.fixes_of ctxt));
    1.44 +    val xs = map #2 (Variable.dest_fixes ctxt);
    1.45      val (Ts, ctxt') = fold_map inferred_param xs ctxt;
    1.46    in (xs ~~ Ts, ctxt') end;
    1.47  
    1.48 @@ -508,7 +495,7 @@
    1.49      val (c, pos) = token_content text;
    1.50      val _ = no_skolem false c;
    1.51    in
    1.52 -    (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    1.53 +    (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
    1.54        (SOME x, false) =>
    1.55          (Context_Position.report ctxt pos
    1.56              (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
    1.57 @@ -524,7 +511,7 @@
    1.58  fun intern_skolem ctxt x =
    1.59    let
    1.60      val _ = no_skolem false x;
    1.61 -    val sko = lookup_skolem ctxt x;
    1.62 +    val sko = Variable.lookup_fixed ctxt x;
    1.63      val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
    1.64      val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
    1.65    in
    1.66 @@ -1061,7 +1048,7 @@
    1.67      val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
    1.68      fun bind (t as Free (x, T)) =
    1.69            if member (op =) xs x then
    1.70 -            (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
    1.71 +            (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t)
    1.72            else t
    1.73        | bind (t $ u) = bind t $ bind u
    1.74        | bind (Abs (x, T, t)) = Abs (x, T, bind t)
    1.75 @@ -1282,8 +1269,8 @@
    1.76          if x = x' then Pretty.str x
    1.77          else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
    1.78        val fixes =
    1.79 -        rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
    1.80 -          (Variable.fixes_of ctxt));
    1.81 +        filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
    1.82 +          (Variable.dest_fixes ctxt);
    1.83        val prt_fixes =
    1.84          if null fixes then []
    1.85          else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::