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