src/Pure/zterm.ML

   | ZThm of {theory_name: string, thm_name: Thm_Name.P, serial: serial};
 
 type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
 
 datatype zproof =
-    ZDummy                         (*dummy proof*)
+    ZNop
   | ZConstp of zproof_const
   | ZBoundp of int
   | ZAbst of string * ztyp * zproof
   | ZAbsp of string * zterm * zproof
   | ZAppt of zproof * zterm

 
 (* fold types/terms within proof *)
 
 fun fold_proof {hyps} typ term =
   let
-    fun proof ZDummy = I
+    fun proof ZNop = I
       | proof (ZConstp (_, (instT, inst))) =
           ZTVars.fold (typ o #2) instT #> ZVars.fold (term o #2) inst
       | proof (ZBoundp _) = I
       | proof (ZAbst (_, T, p)) = typ T #> proof p
       | proof (ZAbsp (_, t, p)) = term t #> proof p

         |> make_inst;
   in if ! changed then (instT', inst') else raise Same.SAME end;
 
 fun map_proof_same {hyps} typ term =
   let
-    fun proof ZDummy = raise Same.SAME
+    fun proof ZNop = raise Same.SAME
       | proof (ZConstp (a, (instT, inst))) =
           ZConstp (a, map_insts_same typ term (instT, inst))
       | proof (ZBoundp _) = raise Same.SAME
       | proof (ZAbst (a, T, p)) =
           (ZAbst (a, typ T, Same.commit proof p)