diff -r adb83939177f -r b59202511b8a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 01 12:30:49 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 01 12:30:50 2005 +0200
@@ -68,8 +68,6 @@
     (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
@@ -635,20 +633,6 @@
 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 =