# HG changeset patch
# User wenzelm
# Date 1154127094 -7200
# Node ID bad805d0456b50461671cf7c1f27c25d2656c3cb
# Parent  6379135f21c2cfe3dcc152aabe226aa5cdb62d52
tuned comment;

diff -r 6379135f21c2 -r bad805d0456b src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jul 29 00:51:33 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Jul 29 00:51:34 2006 +0200
@@ -75,7 +75,7 @@
 
 fun standard ctxt =
   (case #locale (Data.get ctxt) of
-    NONE => map Drule.standard
+    NONE => map Drule.standard   (* FIXME !? *)
   | SOME (_, loc_ctxt) => ProofContext.export_standard ctxt loc_ctxt);