# HG changeset patch
# User wenzelm
# Date 1169394366 -3600
# Node ID 7a8c2a556d28f8337c7aa694069c679248979cf4
# Parent  3b99944136ef09a2180a15a67ace51dad1f6ade8
*** MESSAGE REFERS TO PREVIOUS VERSION ***
removed is_finished_thy;

diff -r 3b99944136ef -r 7a8c2a556d28 src/Pure/context.ML
--- a/src/Pure/context.ML	Sun Jan 21 16:43:47 2007 +0100
+++ b/src/Pure/context.ML	Sun Jan 21 16:46:06 2007 +0100
@@ -681,7 +681,6 @@
 
 end;
 
-
 (*hide private interface*)
 structure Context: CONTEXT = Context;