changeset 33671 | 4b0f2599ed48 |
parent 33515 | d066e8369a33 |
child 35141 | 182f27a8716c |
--- a/src/Pure/Isar/isar_cmd.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Fri Nov 13 21:11:15 2009 +0100 @@ -181,7 +181,7 @@ fun declaration pervasive (txt, pos) = txt |> ML_Context.expression pos "val declaration: Morphism.declaration" - ("Context.map_proof (LocalTheory.declaration " ^ Bool.toString pervasive ^ " declaration)") + ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)") |> Context.proof_map;