variant_fixes: preserve internal state, mark skolem only for body mode;
authorwenzelm
Thu Apr 17 22:22:26 2008 +0200 (2008-04-17)
changeset 267144773b832f1b1
parent 26713 1c6181def1d0
child 26715 00ff79ab6e6b
variant_fixes: preserve internal state, mark skolem only for body mode;
import_inst: actually observe is_open flag (cf. variant_fixes);
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Thu Apr 17 22:22:25 2008 +0200
     1.2 +++ b/src/Pure/variable.ML	Thu Apr 17 22:22:26 2008 +0200
     1.3 @@ -300,8 +300,8 @@
     1.4  fun variant_fixes raw_xs ctxt =
     1.5    let
     1.6      val names = names_of ctxt;
     1.7 -    val xs = map Name.clean raw_xs;
     1.8 -    val (xs', names') = Name.variants xs names |>> map Name.skolem;
     1.9 +    val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
    1.10 +    val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
    1.11    in ctxt |> new_fixes names' xs xs' end;
    1.12  
    1.13  end;
    1.14 @@ -401,7 +401,7 @@
    1.15  
    1.16  fun import_inst is_open ts ctxt =
    1.17    let
    1.18 -    val ren = if is_open then I else Name.internal;
    1.19 +    val ren = Name.clean #> (if is_open then I else Name.internal);
    1.20      val (instT, ctxt') = importT_inst ts ctxt;
    1.21      val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
    1.22      val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';