src/Pure/Isar/isar_cmd.ML
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;