# HG changeset patch # User wenzelm # Date 1140035711 -3600 # Node ID ffbbac0261c9d7c93e383143c3eb619c0086926d # Parent c814a78561215815cacae7553b44a1b196357e1f removed distinct, renamed gen_distinct to distinct; replaced qualified_force_prefix by qualified_names/sticky_prefix; diff -r c814a7856121 -r ffbbac0261c9 src/Pure/Isar/locale.ML --- 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'