src/Pure/Isar/class_target.ML
changeset 35126 ce6544f42eb9
parent 35021 c839a4c670c6
child 35315 fbdc860d87a3
--- 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