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