src/Pure/zterm.ML

 
 datatype zproof_name =
     ZAxiom of string
   | ZOracle of string
   | ZBox of serial
-  | ZThm of {theory_long_name: string, thm_name: Thm_Name.T, pos: Position.T, serial: int};
+  | ZThm of {theory_name: string, thm_name: Thm_Name.T, pos: Position.T, serial: int};
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
   | ZConstp of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
   | ZBoundp of int

 in
 
 fun thm_proof thy (name, pos) =
   let
     val thy_name = Context.theory_long_name thy;
-    fun zproof_name i =
-      ZThm {theory_long_name = thy_name, thm_name = name, pos = pos, serial = i};
+    fun zproof_name i = ZThm {theory_name = thy_name, thm_name = name, pos = pos, serial = i};
   in box_proof zproof_name thy end;
 
 fun add_box_proof thy hyps concl (zboxes, prf) =
   let val (zbox, zbox_prf) = box_proof ZBox thy hyps concl prf
   in (add_zboxes zbox zboxes, zbox_prf) end;