src/Pure/Isar/local_theory.ML

     if b andalso not b' then error "Not at bottom of local theory nesting"
     else if not b andalso b' then error "Already at bottom of local theory nesting"
     else lthy
   end;
 
-fun open_target background_naming operations after_close target =
-  assert target
-  |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+fun open_target background_naming operations after_close lthy =
+  let
+    val _ = assert lthy;
+    val (_, target) = Proof_Context.new_scope lthy;
+  in
+    target |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)))
+  end;
 
 fun close_target lthy =
   let
     val _ = assert_bottom false lthy;
     val ({after_close, ...} :: rest) = Data.get lthy;