# HG changeset patch
# User mengj
# Date 1141959828 -3600
# Node ID 3342e7554b7783bd7ac42b743f79d7189de89390
# Parent  7183628d7b295a045f87a9c9fe481dd50fd144f7
Shortened the exception messages from assume.

diff -r 7183628d7b29 -r 3342e7554b77 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Mar 10 04:02:53 2006 +0100
+++ b/src/Pure/thm.ML	Fri Mar 10 04:03:48 2006 +0100
@@ -619,9 +619,9 @@
 fun assume raw_ct =
   let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx raw_ct in
     if T <> propT then
-      raise THM ("assume: assumptions must have type prop", 0, [])
+      raise THM ("assume: prop", 0, [])
     else if maxidx <> ~1 then
-      raise THM ("assume: assumptions may not contain schematic variables", maxidx, [])
+      raise THM ("assume: variables", maxidx, [])
     else Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' I (false, Pt.Hyp prop),
       maxidx = ~1,