src/Pure/Isar/locale.ML
changeset 30438 c2d49315b93b
parent 30344 10a67c5ddddb
child 30466 5f31e24937c5
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Mar 11 15:45:40 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Mar 11 16:36:27 2009 +0100
     1.3 @@ -107,19 +107,6 @@
     1.4  
     1.5  datatype ctxt = datatype Element.ctxt;
     1.6  
     1.7 -fun global_note_qualified kind facts thy = (*FIXME*)
     1.8 -  thy
     1.9 -  |> Sign.qualified_names
    1.10 -  |> PureThy.note_thmss kind facts
    1.11 -  ||> Sign.restore_naming thy;
    1.12 -
    1.13 -fun local_note_qualified kind facts ctxt = (*FIXME*)
    1.14 -  ctxt
    1.15 -  |> ProofContext.qualified_names
    1.16 -  |> ProofContext.note_thmss_i kind facts
    1.17 -  ||> ProofContext.restore_naming ctxt;
    1.18 -
    1.19 -
    1.20  
    1.21  (*** Theory data ***)
    1.22  
    1.23 @@ -337,7 +324,7 @@
    1.24  fun init_global_elem (Notes (kind, facts)) thy =
    1.25    let
    1.26      val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    1.27 -  in global_note_qualified kind facts' thy |> snd end
    1.28 +  in PureThy.note_thmss kind facts' thy |> snd end
    1.29  
    1.30  fun init_local_elem (Fixes fixes) ctxt = ctxt |>
    1.31        ProofContext.add_fixes_i fixes |> snd
    1.32 @@ -359,7 +346,7 @@
    1.33    | init_local_elem (Notes (kind, facts)) ctxt =
    1.34        let
    1.35          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
    1.36 -      in local_note_qualified kind facts' ctxt |> snd end
    1.37 +      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
    1.38  
    1.39  fun cons_elem false (Notes notes) elems = elems
    1.40    | cons_elem _ elem elems = elem :: elems
    1.41 @@ -452,7 +439,7 @@
    1.42              let
    1.43                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
    1.44                  Attrib.map_facts (Attrib.attribute_i thy)
    1.45 -            in global_note_qualified kind args'' #> snd end)
    1.46 +            in PureThy.note_thmss kind args'' #> snd end)
    1.47          (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
    1.48    in ctxt'' end;
    1.49