tuned comment;
authorwenzelm
Sat, 29 Jul 2006 00:51:34 +0200
changeset 20252 bad805d0456b
parent 20251 6379135f21c2
child 20253 636ac45d100f
tuned comment;
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);