| changeset 24031 | e94e541346d7 |
| parent 24020 | ed4d7abffee7 |
| child 24071 | 82873bc360c2 |
--- a/src/Pure/Isar/isar_cmd.ML Sat Jul 28 22:01:01 2007 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Jul 28 22:01:06 2007 +0200 @@ -233,7 +233,7 @@ (* declarations *) val declaration = - ML_Context.use_let "val declaration: declaration" + ML_Context.use_let "val declaration: Morphism.declaration" "Context.map_proof (LocalTheory.declaration declaration)" #> Context.proof_map;