--- 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])