--- 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 =