1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -833,7 +833,7 @@
     1.4  
     1.5    fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
     1.6      thm_of p
     1.7 -    |> singleton (ProofContext.export inner_ctxt outer_ctxt)
     1.8 +    |> singleton (Proof_Context.export inner_ctxt outer_ctxt)
     1.9      |> discharge_assms (make_discharge_rules rules)
    1.10  in
    1.11