Locale instantiation: label parameter optional, new attribute paramter.

--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 07 14:25:48 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 07 20:42:13 2004 +0200
@@ -359,8 +359,7 @@
 
 val instantiateP =
   OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
-    (P.name --| P.$$$ ":" -- P.xname
-(*    (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *)
+    (P.opt_thm_name ":" -- P.xname
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
 
 

--- a/src/Pure/Isar/isar_thy.ML	Wed Apr 07 14:25:48 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Apr 07 20:42:13 2004 +0200
@@ -48,7 +48,8 @@
   val using_facts_i: (thm * Proof.context attribute list) list list
     -> ProofHistory.T -> ProofHistory.T
   val chain: ProofHistory.T -> ProofHistory.T
-  val instantiate_locale: string * string -> ProofHistory.T -> ProofHistory.T
+  val instantiate_locale: (string * Args.src list) * string -> ProofHistory.T
+    -> ProofHistory.T
   val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
   val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
   val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
@@ -293,8 +294,12 @@
 
 (* locale instantiation *)
 
-fun instantiate_locale (prfx, loc) =
-  ProofHistory.apply (Proof.instantiate_locale (loc, prfx));
+fun instantiate_locale ((name, attribs), loc) =
+  ProofHistory.apply (fn state =>
+    let val thy = Proof.theory_of state
+    in Proof.instantiate_locale (loc, 
+        (name, map (Attrib.local_attribute thy) attribs)) state
+    end);
 
 (* context *)
 

--- a/src/Pure/Isar/locale.ML	Wed Apr 07 14:25:48 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Apr 07 20:42:13 2004 +0200
@@ -65,7 +65,8 @@
   val add_thmss: string -> ((string * thm list) * context attribute list) list ->
     theory * context -> (theory * context) * (string * thm list) list
   val prune_prems: theory -> thm -> thm
-  val instantiate: string -> string -> thm list option -> context -> context
+  val instantiate: string -> string * context attribute list
+    -> thm list option -> context -> context
   val setup: (theory -> theory) list
 end;
 
@@ -1040,7 +1041,7 @@
 
 (** CB: experimental instantiation mechanism **)
 
-fun instantiate loc_name prfx raw_inst ctxt =
+fun instantiate loc_name (prfx, attribs) raw_inst ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val sign = Theory.sign_of thy;
@@ -1052,11 +1053,12 @@
     val {view = (_, axioms), params = (ps, _), ...} =
       the_locale thy (intern sign loc_name);
     val fixed_params = param_types ps;
+    val init = ProofContext.init thy;
     val (ids, raw_elemss) =
-          flatten (ctxt, intern_expr sign) ([], Expr (Locale loc_name));
+          flatten (init, intern_expr sign) ([], Expr (Locale loc_name));
     val ((parms, all_elemss, concl),
          (spec as (_, (ints, _)), (xs, env, defs))) =
-      read_elemss false (* do_close *) ctxt
+      read_elemss false (* do_close *) init
         fixed_params (* could also put [] here??? *) raw_elemss
         [] (* concl *);
 
@@ -1077,7 +1079,15 @@
     val args = case inst of
             None => []
           | Some thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
-              |> Term.strip_comb |> snd;
+              |> Term.strip_comb
+              |>> (fn t as (Const (s, _)) => if (intern sign loc_name = s)
+                        then t
+                        else error ("Constant " ^ quote loc_name ^
+                          " expected but constant " ^ quote s ^ " was found")
+                    | t => error ("Constant " ^ quote loc_name ^ " expected \
+                          \but term " ^ quote (Sign.string_of_term sign t) ^
+                          " was found"))
+              |> snd;
     val cargs = map cert args;
 
     (* process parameters: match their types with those of arguments *)
@@ -1093,7 +1103,8 @@
     val arg_types = map Term.fastype_of args;
     val Tenv = foldl (Type.typ_match tsig)
           (Vartab.empty, v_param_types ~~ arg_types)
-          handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact";
+          handle Library.LIST "~~" => error "Number of parameters does not \
+            \match number of arguments of chained fact";
     (* get their sorts *)
     val tfrees = foldr Term.add_typ_tfrees (param_types, []);
     val Tenv' = map
@@ -1143,7 +1154,7 @@
         val hyps = #hyps (rep_thm thm);
         val ass = map (fn ax => (prop_of ax, ax)) axioms;
         val axs' = foldl (fn (axs, hyp) => 
-              (case assoc (ass, hyp) of None => axs
+              (case gen_assoc (op aconv) (ass, hyp) of None => axs
                  | Some ax => axs @ [ax])) ([], hyps);
         val thm' = Drule.satisfy_hyps axs' thm;
         (* instantiate types *)
@@ -1165,17 +1176,26 @@
                   end;
       in thm''' end;
 
+    val prefix_fact =
+      if prfx = "" then I
+      else (fn "" => ""
+             | s => NameSpace.append prfx s);
+
     fun inst_elem (ctxt, (Ext _)) = ctxt
       | inst_elem (ctxt, (Int (Notes facts))) =
               (* instantiate fact *)
           let val facts' =
-              map (apsnd (map (apfst (map inst_thm')))) facts
+                map (apsnd (map (apfst (map inst_thm')))) facts
+		handle THM (msg, n, thms) => error ("Exception THM " ^
+		  string_of_int n ^ " raised\n" ^
+		  "Note: instantiate does not support old-style locales \
+                  \declared with (open)\n" ^ msg ^ "\n" ^
+		  cat_lines (map string_of_thm thms))
               (* rename fact *)
-              val facts'' =
-              map (apfst (apfst (fn "" => ""
-                                  | s => NameSpace.append prfx s)))
-                  facts'
-          in fst (ProofContext.have_thmss_i facts'' ctxt)
+              val facts'' = map (apfst (apfst prefix_fact)) facts'
+              (* add attributes *)
+              val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
+          in fst (ProofContext.have_thmss_i facts''' ctxt)
           end
       | inst_elem (ctxt, (Int _)) = ctxt;
 
@@ -1412,6 +1432,8 @@
 local
 
 fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy =
+  (* CB: do_pred = false means old-style locale, declared with (open).
+     Old-style locales don't define predicates. *)
   let
     val sign = Theory.sign_of thy;
     val name = Sign.full_name sign bname;

--- a/src/Pure/Isar/proof.ML	Wed Apr 07 14:25:48 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 07 20:42:13 2004 +0200
@@ -65,7 +65,8 @@
     (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 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
@@ -569,15 +570,14 @@
 
 (* locale instantiation *)
 
-fun instantiate_locale (loc_name, prfx) state = let
-    val ctxt = context_of state;
+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 facts)
+    |> map_context (Locale.instantiate loc_name prfx_attribs facts)
   end;
 
 (* fix *)