# HG changeset patch
# User wenzelm
# Date 938803096 -7200
# Node ID de2e468a42c84dcb17119d067d61f923ca0f24cc
# Parent  811022c3837eab88ff5f0f68c9554b178a52b303
tuned comment;

diff -r 811022c3837e -r de2e468a42c8 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Oct 01 20:38:00 1999 +0200
+++ b/src/Pure/Isar/obtain.ML	Fri Oct 01 20:38:16 1999 +0200
@@ -3,7 +3,7 @@
     Author:     Markus Wenzel, TU Muenchen
 
 The 'obtain' language element -- achieves (eliminated) existential
-quantification proof command level.
+quantification at proof command level.
 
 The common case: