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