src/Pure/Isar/class_target.ML
changeset 35126 ce6544f42eb9
parent 35021 c839a4c670c6
child 35315 fbdc860d87a3
     1.1 --- a/src/Pure/Isar/class_target.ML	Sun Feb 14 17:46:28 2010 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Mon Feb 15 14:04:06 2010 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5    (*instances*)
     1.6    val init_instantiation: string list * (string * sort) list * sort
     1.7 -    -> theory -> local_theory
     1.8 +    -> theory -> Proof.context
     1.9    val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
    1.10    val instantiation_instance: (local_theory -> local_theory)
    1.11      -> local_theory -> Proof.state