--- a/src/Pure/Isar/class_target.ML Sun Feb 14 17:46:28 2010 +0100
+++ b/src/Pure/Isar/class_target.ML Mon Feb 15 14:04:06 2010 +0100
@@ -29,7 +29,7 @@
(*instances*)
val init_instantiation: string list * (string * sort) list * sort
- -> theory -> local_theory
+ -> theory -> Proof.context
val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
val instantiation_instance: (local_theory -> local_theory)
-> local_theory -> Proof.state
--- a/src/Pure/Isar/overloading.ML Sun Feb 14 17:46:28 2010 +0100
+++ b/src/Pure/Isar/overloading.ML Mon Feb 15 14:04:06 2010 +0100
@@ -6,7 +6,7 @@
signature OVERLOADING =
sig
- val init: (string * (string * typ) * bool) list -> theory -> local_theory
+ val init: (string * (string * typ) * bool) list -> theory -> Proof.context
val conclude: local_theory -> local_theory
val declare: string * typ -> theory -> term * theory
val confirm: binding -> local_theory -> local_theory