--- a/src/HOL/Proofs/ex/Proof_Terms.thy Sat Apr 09 12:36:25 2016 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy Sat Apr 09 13:28:32 2016 +0200
@@ -46,6 +46,7 @@
ML_val \<open>
val thy = @{theory};
+ val ctxt = @{context};
val prf =
Proof_Syntax.read_proof thy true false
"impI \<cdot> _ \<cdot> _ \<bullet> \
@@ -54,7 +55,7 @@
\ (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
val thm =
prf
- |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
+ |> Reconstruct.reconstruct_proof ctxt @{prop "A \<and> B \<longrightarrow> B \<and> A"}
|> Proof_Checker.thm_of_proof thy
|> Drule.export_without_context;
\<close>