Shortened the exception messages from assume.

--- 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,