src/Pure/Proof/proofchecker.ML

 signature PROOF_CHECKER =
 sig
   val thm_of_proof : theory -> Proofterm.proof -> thm
 end;
 
-structure ProofChecker =
+structure ProofChecker : PROOF_CHECKER =
 struct
 
 open Proofterm;
 
 (***** construct a theorem out of a proof term *****)

             val thm = thm_of ((x, T) :: vs) Hs prf
           in
             Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
           end
 
-      | thm_of vs Hs (prf %% Some t) =
+      | thm_of vs Hs (prf % Some t) =
           let
             val thm = thm_of vs Hs prf
             val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t))
           in Thm.forall_elim ct thm end
 

             val thm = thm_of vs (Thm.assume ct :: Hs) prf
           in
             Thm.implies_intr ct thm
           end
 
-      | thm_of vs Hs (prf % prf') =
+      | thm_of vs Hs (prf %% prf') =
           let 
             val thm = beta_eta_convert (thm_of vs Hs prf);
             val thm' = beta_eta_convert (thm_of vs Hs prf')
           in
             Thm.implies_elim thm thm'