--- a/src/Pure/Isar/locale.ML Wed Feb 15 21:35:11 2006 +0100
+++ b/src/Pure/Isar/locale.ML Wed Feb 15 21:35:11 2006 +0100
@@ -69,11 +69,10 @@
val print_local_registrations': bool -> string -> Proof.context -> unit
val print_local_registrations: bool -> string -> Proof.context -> unit
- (* FIXME avoid duplicates *)
val add_locale: bool -> bstring -> expr -> Element.context list -> theory
- -> Proof.context * theory
+ -> Proof.context (*body context!*) * theory
val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory
- -> Proof.context * theory
+ -> Proof.context (*body context!*) * theory
(* Storing results *)
val note_thmss: string -> xstring ->
@@ -537,10 +536,10 @@
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
in map (Option.map (Envir.norm_type unifier')) Vs end;
-fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
-fun params_of' elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
+fun params_of elemss = distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
+fun params_of' elemss = distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
fun params_syn_of syn elemss =
- gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
+ distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
map (apfst (fn x => (x, the (Symtab.lookup syn x))));
@@ -604,7 +603,7 @@
val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
(Vartab.empty, maxidx);
- val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms);
+ val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
fun inst_parms (i, ps) =
@@ -758,8 +757,8 @@
val ren = renaming xs parms'
handle ERROR msg => err_in_locale' ctxt msg ids';
- val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
- val parms'' = distinct (List.concat (map (#2 o #1) ids''));
+ val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
+ val parms'' = distinct (op =) (List.concat (map (#2 o #1) ids''));
val syn'' = syn' |> Symtab.dest |> map (Element.rename_var ren) |> Symtab.make;
(* check for conflicting syntax? *)
in (ids'', parms'', syn'') end
@@ -1317,7 +1316,7 @@
val (ctxt, (elemss, _)) =
activate_facts prep_facts (import_ctxt, qs);
- val stmt = gen_distinct Term.aconv
+ val stmt = distinct Term.aconv
(List.concat (map (fn ((_, Assumed axs), _) =>
List.concat (map (#hyps o Thm.rep_thm o #2) axs)
| ((_, Derived _), _) => []) qs));
@@ -1377,13 +1376,15 @@
fun global_note_prefix_i kind prfx args thy =
thy
- |> Theory.qualified_force_prefix prfx
+ |> Theory.qualified_names
+ |> Theory.sticky_prefix prfx
|> PureThy.note_thmss_i kind args
||> Theory.restore_naming thy;
fun local_note_prefix_i prfx args ctxt =
ctxt
- |> ProofContext.qualified_force_prefix prfx
+ |> ProofContext.qualified_names
+ |> ProofContext.sticky_prefix prfx
|> ProofContext.note_thmss_i args |> swap
|>> ProofContext.restore_naming ctxt;
@@ -1429,8 +1430,7 @@
Args.map_values I (Element.instT_type (#1 insts))
(Element.inst_term insts) (Element.inst_thm thy insts);
val args' = args |> map (fn ((n, atts), [(ths, [])]) =>
- ((NameSpace.qualified prfx n,
- map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)),
+ ((n, map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)),
[(map (Drule.standard o satisfy_protected prems o
Element.inst_thm thy insts) ths, [])]));
in global_note_prefix_i kind prfx args' thy |> snd end;
@@ -1683,19 +1683,20 @@
(pred_ctxt, axiomify predicate_axioms elemss');
val export = ProofContext.export_view predicate_statement ctxt thy_ctxt;
val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
- val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))
- in
- pred_thy
- |> PureThy.note_thmss_qualified "" bname facts' |> snd
- |> declare_locale name
- |> put_locale name {predicate = predicate, import = import,
+ val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'));
+
+ val thy' = pred_thy
+ |> PureThy.note_thmss_qualified "" bname facts' |> snd
+ |> declare_locale name
+ |> put_locale name
+ {predicate = predicate,
+ import = import,
elems = map (fn e => (e, stamp ())) elems',
params = (params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
map #1 (params_of body_elemss)),
abbrevs = [],
- regs = []}
- |> pair (body_ctxt)
- end;
+ regs = []};
+ in (ProofContext.transfer thy' body_ctxt, thy') end;
in
@@ -1835,9 +1836,7 @@
(* insert interpretation attributes *)
|> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
(* discharge hyps *)
- |> map (apsnd (map (apfst (map disch))))
- (* prefix names *)
- |> map (apfst (apfst (NameSpace.qualified prfx)))
+ |> map (apsnd (map (apfst (map disch))));
in fst (note prfx facts' thy_ctxt) end
| activate_elem _ _ _ thy_ctxt = thy_ctxt;
@@ -2076,7 +2075,6 @@
(disch o Element.inst_thm thy insts o satisfy))
|> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
|> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
- |> map (apfst (apfst (NameSpace.qualified prfx)))
in
thy
|> global_note_prefix_i "" prfx facts'