src/Pure/variable.ML
changeset 20198 7b385487f22f
parent 20162 d4bcb27686f9
child 20220 5dc68e9ecd9a
     1.1 --- a/src/Pure/variable.ML	Tue Jul 25 21:18:04 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Jul 25 21:18:05 2006 +0200
     1.3 @@ -297,9 +297,9 @@
     1.4  
     1.5  fun import_inst is_open ts ctxt =
     1.6    let
     1.7 +    val ren = if is_open then I else Name.internal;
     1.8      val (instT, ctxt') = importT_inst ts ctxt;
     1.9      val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
    1.10 -    val ren = if is_open then I else Name.internal;
    1.11      val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
    1.12      val inst = vars ~~ map Free (xs ~~ map #2 vars);
    1.13    in ((instT, inst), ctxt'') end;