# HG changeset patch
# User haftmann
# Date 1266239046 -3600
# Node ID ce6544f42eb9807ad951a04b78f1195dd91faa6c
# Parent  acace7e303574f252688dc3b0a0eaae7ea989fb7
clarifed type

diff -r acace7e30357 -r ce6544f42eb9 src/Pure/Isar/class_target.ML
--- 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
diff -r acace7e30357 -r ce6544f42eb9 src/Pure/Isar/overloading.ML
--- 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