# HG changeset patch
# User nipkow
# Date 1527680693 -7200
# Node ID 57e4bd1e2e189211de99d0a1d517bf26f064d737
# Parent  88c07fabd5b411422dba001138ac334c426a1fdd
unused

diff -r 88c07fabd5b4 -r 57e4bd1e2e18 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 29 22:29:32 2018 +0200
+++ b/src/HOL/List.thy	Wed May 30 13:44:53 2018 +0200
@@ -429,7 +429,6 @@
   (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
   "_lc_end" :: "lc_quals" ("]")
   "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")
-  "_lc_abs" :: "'a => 'b list => 'b list"
 
 syntax (ASCII)
   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")