revert_skolem: do not change non-reversible names;
authorwenzelm
Thu Apr 17 22:22:30 2008 +0200 (2008-04-17 ago)
changeset 267172e1c3a0e7308
parent 26716 8690e75e1395
child 26718 0c652e82fdf4
revert_skolem: do not change non-reversible names;
default token translations: revert_skolem;
removed obsolete revert_skolems;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 17 22:22:28 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 17 22:22:30 2008 +0200
     1.3 @@ -49,7 +49,6 @@
     1.4    val cert_typ_abbrev: Proof.context -> typ -> typ
     1.5    val get_skolem: Proof.context -> string -> string
     1.6    val revert_skolem: Proof.context -> string -> string
     1.7 -  val revert_skolems: Proof.context -> term -> term
     1.8    val infer_type: Proof.context -> string -> typ
     1.9    val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
    1.10    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
    1.11 @@ -347,37 +346,21 @@
    1.12    else x;
    1.13  
    1.14  
    1.15 -(* revert Skolem constants -- approximation only! *)
    1.16 +(* revert Skolem constants -- if possible *)
    1.17  
    1.18 -fun revert_skolem ctxt =
    1.19 -  let
    1.20 -    val rev_fixes = map Library.swap (Variable.fixes_of ctxt);
    1.21 -    val revert = AList.lookup (op =) rev_fixes;
    1.22 -  in
    1.23 -    fn x =>
    1.24 -      (case revert x of
    1.25 -        SOME x' => x'
    1.26 -      | NONE => perhaps (try Name.dest_skolem) x)
    1.27 -   end;
    1.28 -
    1.29 -fun revert_skolems ctxt =
    1.30 -  let
    1.31 -    val revert = revert_skolem ctxt;
    1.32 -    fun reverts (Free (x, T)) = Free (revert x, T)
    1.33 -      | reverts (t $ u) = reverts t $ reverts u
    1.34 -      | reverts (Abs (x, T, t)) = Abs (x, T, reverts t)
    1.35 -      | reverts a = a;
    1.36 -  in reverts end;
    1.37 +fun revert_skolem ctxt x =
    1.38 +  (case find_first (fn (_, y) => y = x) (Variable.fixes_of ctxt) of
    1.39 +    SOME (x', _) => if lookup_skolem ctxt x' = SOME x then x' else x
    1.40 +  | NONE => x);
    1.41  
    1.42  
    1.43  (* default token translations *)
    1.44  
    1.45  local
    1.46  
    1.47 -fun free_or_skolem ctxt x =   (* FIXME revert skolem *)
    1.48 -  (case try Name.dest_skolem x of
    1.49 -    NONE => Pretty.mark Markup.free (Pretty.str x)
    1.50 -  | SOME x' => Pretty.mark Markup.skolem (Pretty.str x'))
    1.51 +fun free_or_skolem ctxt x =
    1.52 +  (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
    1.53 +   else Pretty.mark Markup.free (Pretty.str x))
    1.54    |> Pretty.mark (if Variable.is_fixed ctxt x then Markup.fixed x else Markup.hilite);
    1.55  
    1.56  fun var_or_skolem _ s =