diff -r deadcd0ec431 -r e6bb250402b5 src/Pure/variable.ML
--- 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 =