1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -297,7 +297,7 @@
     1.4  fun extern_fact ctxt name =
     1.5    let
     1.6      val local_facts = facts_of ctxt;
     1.7 -    val global_facts = PureThy.facts_of (theory_of ctxt);
     1.8 +    val global_facts = Global_Theory.facts_of (theory_of ctxt);
     1.9    in
    1.10      if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
    1.11      then Facts.extern local_facts name
    1.12 @@ -790,7 +790,7 @@
    1.13        extern_const = Consts.extern consts};
    1.14    in
    1.15      Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
    1.16 -      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax (theory_of ctxt)))
    1.17 +      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt)))
    1.18    end;
    1.19  
    1.20  in
    1.21 @@ -982,7 +982,7 @@
    1.22                SOME (_, ths) =>
    1.23                 (Context_Position.report ctxt pos (Markup.local_fact name);
    1.24                  map (Thm.transfer thy) (Facts.select thmref ths))
    1.25 -            | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
    1.26 +            | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
    1.27        in pick name thms end;
    1.28  
    1.29  in
    1.30 @@ -1012,12 +1012,12 @@
    1.31      val name = full_name ctxt b;
    1.32      val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
    1.33  
    1.34 -    val facts = PureThy.name_thmss false name raw_facts;
    1.35 +    val facts = Global_Theory.name_thmss false name raw_facts;
    1.36      fun app (th, attrs) x =
    1.37        swap (Library.foldl_map
    1.38          (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
    1.39      val (res, ctxt') = fold_map app facts ctxt;
    1.40 -    val thms = PureThy.name_thms false false name (flat res);
    1.41 +    val thms = Global_Theory.name_thms false false name (flat res);
    1.42      val Mode {stmt, ...} = get_mode ctxt;
    1.43    in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
    1.44