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/HOL/Nominal/nominal_fresh_fun.ML
changeset 42361 23f352990944
parent 41519 0940fff556a6
child 42364 8c674b3b8e44 
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -125,7 +125,7 @@
   (* Find the variable we instantiate *)
   let
     val thy = theory_of_thm thm;
-    val ctxt = ProofContext.init_global thy;
+    val ctxt = Proof_Context.init_global thy;
     val ss = global_simpset_of thy;
     val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
     val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
isabelle