# HG changeset patch
# User paulson
# Date 1077183661 -3600
# Node ID 011a2a49d3033994f70a43f0e75a385375c4d12b
# Parent  cc96cc06abf9d112674c174cc8d93703a45a603e
removed a reference to the ML structure List.thy

diff -r cc96cc06abf9 -r 011a2a49d303 src/HOL/TLA/Buffer/Buffer.ML
--- a/src/HOL/TLA/Buffer/Buffer.ML	Thu Feb 19 10:40:28 2004 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.ML	Thu Feb 19 10:41:01 2004 +0100
@@ -8,8 +8,8 @@
 
 (* ---------------------------- Data lemmas ---------------------------- *)
 
-context List.thy;
-goal List.thy "xs ~= [] --> tl xs ~= xs";
+(*FIXME: move to List.thy? Maybe as (tl xs = xs) = (xs = [])"?*)
+Goal "xs ~= [] --> tl xs ~= xs";
 by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv]));
 qed_spec_mp "tl_not_self";
 context Buffer.thy;