changeset 42361 | 23f352990944 |
parent 42318 | 0fd33b6b22cf |
child 42793 | 88bee9f6eec7 |
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Apr 16 16:15:37 2011 +0200 @@ -833,7 +833,7 @@ fun discharge rules outer_ctxt (p, (inner_ctxt, _)) = thm_of p - |> singleton (ProofContext.export inner_ctxt outer_ctxt) + |> singleton (Proof_Context.export inner_ctxt outer_ctxt) |> discharge_assms (make_discharge_rules rules) in