1.1 --- a/src/Pure/Isar/attrib.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  
     1.5  fun print_attributes thy =
     1.6    let
     1.7 -    val ctxt = ProofContext.init_global thy;
     1.8 +    val ctxt = Proof_Context.init_global thy;
     1.9      val attribs = Attributes.get thy;
    1.10      fun prt_attr (name, (_, comment)) = Pretty.block
    1.11        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.12 @@ -91,7 +91,7 @@
    1.13  val intern = Name_Space.intern o #1 o Attributes.get;
    1.14  val intern_src = Args.map_name o intern;
    1.15  
    1.16 -fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (ProofContext.theory_of ctxt)));
    1.17 +fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (Proof_Context.theory_of ctxt)));
    1.18  
    1.19  
    1.20  (* pretty printing *)
    1.21 @@ -130,8 +130,8 @@
    1.22  (* fact expressions *)
    1.23  
    1.24  fun eval_thms ctxt srcs = ctxt
    1.25 -  |> ProofContext.note_thmss ""
    1.26 -    (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
    1.27 +  |> Proof_Context.note_thmss ""
    1.28 +    (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt)
    1.29        [((Binding.empty, []), srcs)])
    1.30    |> fst |> maps snd;
    1.31  
    1.32 @@ -143,7 +143,7 @@
    1.33    thm structure.*)
    1.34  
    1.35  fun crude_closure ctxt src =
    1.36 - (try (fn () => attribute_i (ProofContext.theory_of ctxt) src
    1.37 + (try (fn () => attribute_i (Proof_Context.theory_of ctxt) src
    1.38      (Context.Proof ctxt, Drule.asm_rl)) ();
    1.39    Args.closure src);
    1.40  
    1.41 @@ -185,7 +185,7 @@
    1.42  fun gen_thm pick = Scan.depend (fn context =>
    1.43    let
    1.44      val thy = Context.theory_of context;
    1.45 -    val get = Context.cases (Global_Theory.get_fact context) ProofContext.get_fact context;
    1.46 +    val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
    1.47      val get_fact = get o Facts.Fact;
    1.48      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
    1.49    in
    1.50 @@ -336,7 +336,7 @@
    1.51  
    1.52  fun print_configs ctxt =
    1.53    let
    1.54 -    val thy = ProofContext.theory_of ctxt;
    1.55 +    val thy = Proof_Context.theory_of ctxt;
    1.56      fun prt (name, config) =
    1.57        let val value = Config.get ctxt config in
    1.58          Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
    1.59 @@ -413,7 +413,7 @@
    1.60    register_config Name_Space.short_names_raw #>
    1.61    register_config Name_Space.unique_names_raw #>
    1.62    register_config ML_Context.trace_raw #>
    1.63 -  register_config ProofContext.show_abbrevs_raw #>
    1.64 +  register_config Proof_Context.show_abbrevs_raw #>
    1.65    register_config Goal_Display.goals_limit_raw #>
    1.66    register_config Goal_Display.show_main_goal_raw #>
    1.67    register_config Goal_Display.show_consts_raw #>