src/Pure/Isar/proof.ML

     (thmref * 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: ((thmref * 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 * context attribute list) -> 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 using_thmss_i = gen_using_thmss ProofContext.note_thmss_i;
 
 end;
 
 
-(* locale instantiation *)
-
-fun instantiate_locale (loc_name, prfx_attribs) state =
-  let
-    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_attribs facts)
-  end;
-
-
 (* fix *)
 
 fun gen_fix f xs state =
   state
   |> assert_forward