# HG changeset patch
# User haftmann
# Date 1288888057 -3600
# Node ID c409827db57d3fbd370cf676432dc69350a2aa2b
# Parent  1a73b5b90a3cd380b643707fdba1158471c961cc
corrected quoting

diff -r 1a73b5b90a3c -r c409827db57d src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Thu Nov 04 17:27:37 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy	Thu Nov 04 17:27:37 2010 +0100
@@ -146,7 +146,7 @@
   "_sdo_block (_sdo_final e)" => "e"
 
 text {*
-  For an example, see @{text HOL/Proofs/Extraction/Higman.thy}.
+  For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
 *}
 
 end