--- a/src/HOL/Tools/choice_specification.ML Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/choice_specification.ML Sat Apr 16 16:15:37 2011 +0200
@@ -220,11 +220,11 @@
|> process_all (zip3 alt_names rew_imps frees)
end
- fun after_qed [[thm]] = ProofContext.background_theory (fn thy =>
+ fun after_qed [[thm]] = Proof_Context.background_theory (fn thy =>
#1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
in
thy
- |> ProofContext.init_global
+ |> Proof_Context.init_global
|> Variable.declare_term ex_prop
|> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
end;