tuned;
authorwenzelm
Tue Jul 25 21:18:05 2006 +0200 (2006-07-25)
changeset 201987b385487f22f
parent 20197 ffc64d90fc1f
child 20199 3170fea83ae7
tuned;
src/Pure/name.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/name.ML	Tue Jul 25 21:18:04 2006 +0200
     1.2 +++ b/src/Pure/name.ML	Tue Jul 25 21:18:05 2006 +0200
     1.3 @@ -99,8 +99,9 @@
     1.4            end;
     1.5    in invs o clean end;
     1.6  
     1.7 +fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
     1.8 +
     1.9  val invent_list = invents o make_context;
    1.10 -fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
    1.11  
    1.12  
    1.13  (* variants *)
     2.1 --- a/src/Pure/variable.ML	Tue Jul 25 21:18:04 2006 +0200
     2.2 +++ b/src/Pure/variable.ML	Tue Jul 25 21:18:05 2006 +0200
     2.3 @@ -297,9 +297,9 @@
     2.4  
     2.5  fun import_inst is_open ts ctxt =
     2.6    let
     2.7 +    val ren = if is_open then I else Name.internal;
     2.8      val (instT, ctxt') = importT_inst ts ctxt;
     2.9      val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
    2.10 -    val ren = if is_open then I else Name.internal;
    2.11      val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
    2.12      val inst = vars ~~ map Free (xs ~~ map #2 vars);
    2.13    in ((instT, inst), ctxt'') end;