src/Pure/Isar/element.ML
changeset 19466 29bc35832a77
parent 19305 5c16895d548b
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/Isar/element.ML	Tue Apr 25 22:23:30 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Apr 25 22:23:41 2006 +0200
     1.3 @@ -326,12 +326,11 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6      val th = Goal.norm_hhf raw_th;
     1.7 -    val maxidx = #maxidx (Thm.rep_thm th);
     1.8  
     1.9      fun standard_thesis t =
    1.10        let
    1.11          val C = ObjectLogic.drop_judgment thy (Thm.concl_of th);
    1.12 -        val C' = Var ((AutoBind.thesisN, maxidx + 1), Term.fastype_of C);
    1.13 +        val C' = Var ((AutoBind.thesisN, Thm.maxidx_of th + 1), Term.fastype_of C);
    1.14        in Term.subst_atomic [(C, C')] t end;
    1.15  
    1.16      val raw_prop =