src/Pure/Isar/proof.ML

     (xstring * context attribute list) list) list -> state -> state
   val with_thmss_i: ((bstring * context attribute list) *
     (thm list * context attribute list) list) list -> state -> state
   val using_thmss: ((xstring * context attribute list) list) list -> state -> state
   val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
+  val instantiate_locale: string * string -> state -> state
   val fix: (string list * string option) list -> state -> state
   val fix_i: (string list * typ option) list -> state -> state
   val assm: ProofContext.exporter
     -> ((string * context attribute list) * (string * (string list * string list)) list) list
     -> state -> state

 val let_bind = gen_bind (ProofContext.match_bind true);
 val let_bind_i = gen_bind (ProofContext.match_bind_i true);
 
 
 (* have_thmss *)
+(* CB: this implements "note" of the Isar/VM *)
 
 local
 
 fun gen_have_thmss f args state =
   state

 val using_thmss = gen_using_thmss ProofContext.have_thmss;
 val using_thmss_i = gen_using_thmss ProofContext.have_thmss_i;
 
 end;
 
+
+(* locale instantiation *)
+
+fun instantiate_locale (loc_name, prfx) state = let
+    val ctxt = context_of state;
+    val facts = if is_chain state then get_facts state else None;
+  in
+    state
+    |> assert_forward_or_chain
+    |> enter_forward
+    |> reset_facts
+    |> map_context (Locale.instantiate loc_name prfx facts)
+  end;
 
 (* fix *)
 
 fun gen_fix f xs state =
   state