--- a/Nominal/nominal_library.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_library.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -154,7 +154,7 @@
 
 (* testing for concrete atom types *)
 fun is_atom ctxt ty =
-  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
+  Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort at_base})
 
 fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty
   | is_atom_set _ _ = false;