--- a/src/Pure/thm.ML Wed Aug 19 10:49:30 1998 +0200
+++ b/src/Pure/thm.ML Wed Aug 19 17:04:21 1998 +0200
@@ -653,15 +653,15 @@
val disch = gen_rem (op aconv);
(*The assumption rule A|-A in a theory*)
-fun assume ct : thm =
- let val Cterm {sign_ref, t=prop, T, maxidx} = ct
+fun assume raw_ct : thm =
+ let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
in if T<>propT then
raise THM("assume: assumptions must have type prop", 0, [])
else if maxidx <> ~1 then
raise THM("assume: assumptions may not contain scheme variables",
maxidx, [])
else Thm{sign_ref = sign_ref,
- der = infer_derivs (Assume ct, []),
+ der = infer_derivs (Assume ct, []),
maxidx = ~1,
shyps = add_term_sorts(prop,[]),
hyps = [prop],