--- a/src/Pure/Isar/specification.ML Fri Oct 12 20:21:56 2007 +0200
+++ b/src/Pure/Isar/specification.ML Fri Oct 12 20:21:57 2007 +0200
@@ -299,8 +299,9 @@
val (loc, ctxt, lthy) =
(case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
- (SOME loc, true) => (* workaround non-modularity of in/includes *) (* FIXME *)
- (SOME loc, ProofContext.init thy, LocalTheory.restore lthy0)
+ ({target, is_locale = true, ...}, true) =>
+ (*temporary workaround for non-modularity of in/includes*) (* FIXME *)
+ (SOME target, ProofContext.init thy, LocalTheory.restore lthy0)
| _ => (NONE, lthy0, lthy0));
val attrib = prep_att thy;