src/Pure/Isar/locale.ML
changeset 26645 e114be97befe
parent 26634 149f80f27c84
child 26948 efe3e0e235d6
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Apr 14 16:42:47 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Apr 14 17:54:56 2008 +0200
     1.3 @@ -637,7 +637,8 @@
     1.4    distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
     1.5  
     1.6  
     1.7 -fun params_prefix params = space_implode "_" params;
     1.8 +fun params_qualified params name =
     1.9 +  NameSpace.qualified (space_implode "_" params) name;
    1.10  
    1.11  
    1.12  (* CB: param_types has the following type:
    1.13 @@ -939,7 +940,7 @@
    1.14          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
    1.15          val elem_morphism =
    1.16            Element.rename_morphism ren $>
    1.17 -          Morphism.name_morphism (NameSpace.qualified (params_prefix params)) $>
    1.18 +          Morphism.name_morphism (params_qualified params) $>
    1.19            Element.instT_morphism thy env;
    1.20          val elems' = map (Element.morph_ctxt elem_morphism) elems;
    1.21        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
    1.22 @@ -1583,16 +1584,18 @@
    1.23  
    1.24  (* naming of interpreted theorems *)
    1.25  
    1.26 -fun global_note_prefix_i kind (fully_qualified, prfx) args thy =
    1.27 +fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
    1.28    thy
    1.29    |> Sign.qualified_names
    1.30 +  |> Sign.add_path (NameSpace.base loc ^ "_locale")
    1.31    |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    1.32    |> PureThy.note_thmss_i kind args
    1.33    ||> Sign.restore_naming thy;
    1.34  
    1.35 -fun local_note_prefix_i kind (fully_qualified, prfx) args ctxt =
    1.36 +fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
    1.37    ctxt
    1.38    |> ProofContext.qualified_names
    1.39 +  |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
    1.40    |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
    1.41    |> ProofContext.note_thmss_i kind args
    1.42    ||> ProofContext.restore_naming ctxt;
    1.43 @@ -1696,7 +1699,7 @@
    1.44          val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
    1.45          val attrib = Attrib.attribute_i thy;
    1.46          val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args;
    1.47 -      in global_note_prefix_i kind (fully_qualified, prfx) args' thy |> snd end;
    1.48 +      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
    1.49    in fold activate regs thy end;
    1.50  
    1.51  
    1.52 @@ -2077,14 +2080,14 @@
    1.53      val (propss, eq_props) = chop (length new_elemss) propss;
    1.54      val (thmss, eq_thms) = chop (length new_elemss) thmss;
    1.55  
    1.56 -    fun activate_elem prems eqns exp ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
    1.57 +    fun activate_elem prems eqns exp loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
    1.58          let
    1.59            val ctxt = mk_ctxt thy_ctxt;
    1.60            val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
    1.61                (Symtab.empty, Symtab.empty) prems eqns atts
    1.62                exp (attrib thy_ctxt) facts;
    1.63 -        in snd (note_interp kind (fully_qualified, prfx) facts' thy_ctxt) end
    1.64 -      | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
    1.65 +        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
    1.66 +      | activate_elem _ _ _ _ _ _ thy_ctxt = thy_ctxt;
    1.67  
    1.68      fun activate_elems prems eqns exp ((id, _), elems) thy_ctxt =
    1.69        let
    1.70 @@ -2092,7 +2095,7 @@
    1.71           of SOME x => x
    1.72            | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
    1.73                ^ " while activating facts.");
    1.74 -      in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp prfx_atts) elems thy_ctxt end;
    1.75 +      in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp (fst id) prfx_atts) elems thy_ctxt end;
    1.76  
    1.77      val thy_ctxt' = thy_ctxt
    1.78        (* add registrations *)
    1.79 @@ -2373,7 +2376,7 @@
    1.80                          disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
    1.81                end;
    1.82  
    1.83 -            fun activate_elem (Notes (kind, facts)) thy =
    1.84 +            fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
    1.85                  let
    1.86                    val att_morphism =
    1.87                      Morphism.name_morphism (NameSpace.qualified prfx) $>
    1.88 @@ -2386,12 +2389,12 @@
    1.89                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
    1.90                  in
    1.91                    thy
    1.92 -                  |> global_note_prefix_i kind (fully_qualified, prfx) facts'
    1.93 +                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
    1.94                    |> snd
    1.95                  end
    1.96 -              | activate_elem _ thy = thy;
    1.97 -
    1.98 -            fun activate_elems (_, elems) thy = fold activate_elem elems thy;
    1.99 +              | activate_elem _ _ thy = thy;
   1.100 +
   1.101 +            fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
   1.102  
   1.103            in thy |> fold activate_assumed_id ids_elemss_thmss
   1.104                   |> fold activate_derived_id ids_elemss