Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Proof/proof_checker.ML
changeset 74411 20b0b27bc6c7
parent 74282 c2ee8d993d6a
child 79134 5f0bbed1c606 
--- a/src/Pure/Proof/proof_checker.ML	Sat Oct 02 12:45:51 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Sat Oct 02 12:59:16 2021 +0200
@@ -72,7 +72,8 @@
   let val lookup = lookup_thm thy in
     fn prf =>
       let
-        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees prf Name.context;
+        val prf_names =
+          Name.build_context (prf |> Proofterm.fold_proof_terms Term.declare_term_frees);
 
         fun thm_of_atom thm Ts =
           let
isabelle