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