# HG changeset patch
# User haftmann
# Date 1236783410 -3600
# Node ID 0c7e1578036c427aeddadbe2fd8253ddc465146e
# Parent  955190fa639b23a80e027ba22c793dae14275154
tuned funny error message

diff -r 955190fa639b -r 0c7e1578036c src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Mar 11 15:56:49 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Mar 11 15:56:50 2009 +0100
@@ -428,7 +428,7 @@
    in
     fun provein x S = 
      case term_of S of
-        Const(@{const_name Set.empty}, _) => error "Unexpected error in Cooper please email Amine Chaieb"
+        Const(@{const_name Set.empty}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
       | Const(@{const_name insert}, _) $ y $ _ => 
          let val (cy,S') = Thm.dest_binop S
          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1