--- a/src/Pure/Isar/expression.ML Wed Sep 02 14:11:45 2009 +0200
+++ b/src/Pure/Isar/expression.ML Thu Sep 03 15:39:02 2009 +0200
@@ -839,7 +839,7 @@
fun gen_sublocale prep_expr intern raw_target expression thy =
let
val target = intern thy raw_target;
- val target_ctxt = Locale.init target thy;
+ val target_ctxt = TheoryTarget.init (SOME target) thy;
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
fun after_qed witss = ProofContext.theory
(fold (fn ((dep, morph), wits) => Locale.add_dependency