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