| changeset 20252 | bad805d0456b |
| parent 20243 | 8b64a1ea9b1b |
| child 20778 | f39c733f2a7e |
--- 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);