--- a/src/Pure/variable.ML Tue May 04 11:02:50 2010 +0200
+++ b/src/Pure/variable.ML Tue May 04 12:30:15 2010 +0200
@@ -376,9 +376,9 @@
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
val tfrees = mk_tfrees [];
val idx = Proofterm.maxidx_proof prf ~1 + 1;
- val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
- val gen_typ = Term_Subst.generalizeT_option tfrees idx;
- in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
+ val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
+ val gen_typ = Term_Subst.generalizeT_same tfrees idx;
+ in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
fun gen_export (mk_tfrees, frees) ths =