# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263509477 -3600
# Node ID eb84e8ca214fa57928b6c58231949597f60b956b
# Parent  fe7d27e197e5fdb78a1d3d3abd3e8b0c5e72531c
trivial

diff -r fe7d27e197e5 -r eb84e8ca214f Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Jan 14 23:48:31 2010 +0100
+++ b/Quot/quotient_info.ML	Thu Jan 14 23:51:17 2010 +0100
@@ -219,8 +219,7 @@
     | SOME l =>
       (case (find_first matches l) of
         SOME x => x
-      | NONE => raise NotFound
-      )
+      | NONE => raise NotFound)
   end
 
 fun print_qconstinfo ctxt =