# HG changeset patch
# User wenzelm
# Date 1538404845 -7200
# Node ID 0b0c3dfd730f27aa358d10efd50807f5db43c106
# Parent  d44cb8a3e5e0a578183155719b09e33dbe1d1da9
tuned;

diff -r d44cb8a3e5e0 -r 0b0c3dfd730f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Oct 01 12:41:35 2018 +0200
+++ b/src/Pure/drule.ML	Mon Oct 01 16:40:45 2018 +0200
@@ -141,7 +141,7 @@
 
 (*cterm version of list_implies: [A1,...,An], B  goes to \<lbrakk>A1;...;An\<rbrakk>\<Longrightarrow>B *)
 fun list_implies([], B) = B
-  | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
+  | list_implies(A::As, B) = mk_implies (A, list_implies(As,B));
 
 (*cterm version of list_comb: maps  (f, [t1,...,tn])  to  f(t1,...,tn) *)
 fun list_comb (f, []) = f