src/Pure/name.ML
changeset 20198 7b385487f22f
parent 20192 956cd30ef3be
child 21565 bd28361f4c5b
     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 *)