src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -65,6 +65,7 @@
     (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
@@ -510,6 +511,7 @@
 
 
 (* have_thmss *)
+(* CB: this implements "note" of the Isar/VM *)
 
 local
 
@@ -565,6 +567,19 @@
 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 =