diff -r e6093a7fa53a -r 29bc35832a77 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Isar/element.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -326,12 +326,11 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val th = Goal.norm_hhf raw_th;
-    val maxidx = #maxidx (Thm.rep_thm th);
 
     fun standard_thesis t =
       let
         val C = ObjectLogic.drop_judgment thy (Thm.concl_of th);
-        val C' = Var ((AutoBind.thesisN, maxidx + 1), Term.fastype_of C);
+        val C' = Var ((AutoBind.thesisN, Thm.maxidx_of th + 1), Term.fastype_of C);
       in Term.subst_atomic [(C, C')] t end;
 
     val raw_prop =