diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -127,7 +127,7 @@
 
 fun import_function_data t ctxt =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ct = cterm_of thy t
     val inst_morph = lift_morphism thy o Thm.instantiate
 
@@ -277,7 +277,7 @@
         plural " " "s " not_defined ^ commas_quote not_defined)
 
     fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
+      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
       orelse error (cat_lines
       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])