1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Nov 12 15:56:10 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Nov 12 15:56:11 2010 +0100
     1.3 @@ -787,7 +787,7 @@
     1.4      | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
     1.5  
     1.6        (* theory rules *)
     1.7 -    | (P.ThLemma, _) =>
     1.8 +    | (P.ThLemma _, _) =>  (* FIXME: use arguments *)
     1.9          (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
    1.10      | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
    1.11      | (P.RewriteStar, ps) =>