src/Pure/proofterm.ML

 
   datatype proof =
      PBound of int
    | Abst of string * typ option * proof
    | AbsP of string * term option * proof
-   | op % of proof * term option
-   | op %% of proof * proof
+   | % of proof * term option
+   | %% of proof * proof
    | Hyp of term
    | PThm of (string * (string * string list) list) * proof * term * typ list option
    | PAxm of string * term * typ list option
    | Oracle of string * term * typ list option
    | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;