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