# HG changeset patch
# User wenzelm
# Date 924277726 -7200
# Node ID 932f27366c8fa2f7d8f6c12db66931243f82b22b
# Parent  83d8dabdae9a9427f67bd403e4827cc0e451edff
and_list;

diff -r 83d8dabdae9a -r 932f27366c8f src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Apr 16 17:48:31 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 16 17:48:46 1999 +0200
@@ -203,7 +203,7 @@
         (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
   in Thm.instantiate (cenvT, cenv) thm end;
 
-fun insts x = Scan.lift (Args.enum "and" (Args.var --| Args.$$$ "=" -- Args.name)) x;
+fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x;
 
 fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of));