src/HOL/Tools/SMT/z3_proof_reconstruction.ML

     | (P.DestEqRes, _) => (dest_eq_res cx ct, cxp)
     | (P.QuantInst, _) => (quant_inst ct, cxp)
     | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
 
       (* theory rules *)
-    | (P.ThLemma, _) =>
+    | (P.ThLemma _, _) =>  (* FIXME: use arguments *)
         (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
     | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
     | (P.RewriteStar, ps) =>
         (rewrite cx simpset (map fst ps) ct, cxp)