modernized structure Proof_Context;
authorwenzelm
Sat Apr 16 15:47:52 2011 +0200 (2011-04-16)
changeset 42360da8817d01e7c
parent 42359 6ca5407863ed
child 42361 23f352990944
modernized structure Proof_Context;
NEWS
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/code.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/skip_proof.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/toplevel.ML
src/Pure/Isar/typedecl.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/context.ML
src/Pure/goal.ML
src/Pure/pure_setup.ML
src/Pure/raw_simplifier.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
src/Pure/subgoal.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type_infer.ML
src/Pure/variable.ML
     1.1 --- a/NEWS	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/NEWS	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -84,6 +84,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Structure Proof_Context follows standard naming scheme.  Old
     1.8 +ProofContext is still available for some time as legacy alias.
     1.9 +
    1.10  * Structure Timing provides various operations for timing; supersedes
    1.11  former start_timing/end_timing etc.
    1.12  
     2.1 --- a/src/Pure/Isar/args.ML	Sat Apr 16 15:25:25 2011 +0200
     2.2 +++ b/src/Pure/Isar/args.ML	Sat Apr 16 15:47:52 2011 +0200
     2.3 @@ -184,25 +184,25 @@
     2.4  
     2.5  (* terms and types *)
     2.6  
     2.7 -val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
     2.8 +val typ_abbrev = Scan.peek (named_typ o Proof_Context.read_typ_abbrev o Context.proof_of);
     2.9  val typ = Scan.peek (named_typ o Syntax.read_typ o Context.proof_of);
    2.10  val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of);
    2.11 -val term_abbrev = Scan.peek (named_term o ProofContext.read_term_abbrev o Context.proof_of);
    2.12 +val term_abbrev = Scan.peek (named_term o Proof_Context.read_term_abbrev o Context.proof_of);
    2.13  val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of);
    2.14  
    2.15  
    2.16  (* type and constant names *)
    2.17  
    2.18  fun type_name strict =
    2.19 -  Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict))
    2.20 +  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) strict))
    2.21    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    2.22  
    2.23  fun const strict =
    2.24 -  Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict dummyT))
    2.25 +  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) strict dummyT))
    2.26    >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
    2.27  
    2.28  fun const_proper strict =
    2.29 -  Scan.peek (fn ctxt => named_term (ProofContext.read_const_proper (Context.proof_of ctxt) strict))
    2.30 +  Scan.peek (fn ctxt => named_term (Proof_Context.read_const_proper (Context.proof_of ctxt) strict))
    2.31    >> (fn Const (c, _) => c | _ => "");
    2.32  
    2.33  
     3.1 --- a/src/Pure/Isar/attrib.ML	Sat Apr 16 15:25:25 2011 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Sat Apr 16 15:47:52 2011 +0200
     3.3 @@ -73,7 +73,7 @@
     3.4  
     3.5  fun print_attributes thy =
     3.6    let
     3.7 -    val ctxt = ProofContext.init_global thy;
     3.8 +    val ctxt = Proof_Context.init_global thy;
     3.9      val attribs = Attributes.get thy;
    3.10      fun prt_attr (name, (_, comment)) = Pretty.block
    3.11        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    3.12 @@ -91,7 +91,7 @@
    3.13  val intern = Name_Space.intern o #1 o Attributes.get;
    3.14  val intern_src = Args.map_name o intern;
    3.15  
    3.16 -fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (ProofContext.theory_of ctxt)));
    3.17 +fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (Proof_Context.theory_of ctxt)));
    3.18  
    3.19  
    3.20  (* pretty printing *)
    3.21 @@ -130,8 +130,8 @@
    3.22  (* fact expressions *)
    3.23  
    3.24  fun eval_thms ctxt srcs = ctxt
    3.25 -  |> ProofContext.note_thmss ""
    3.26 -    (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
    3.27 +  |> Proof_Context.note_thmss ""
    3.28 +    (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt)
    3.29        [((Binding.empty, []), srcs)])
    3.30    |> fst |> maps snd;
    3.31  
    3.32 @@ -143,7 +143,7 @@
    3.33    thm structure.*)
    3.34  
    3.35  fun crude_closure ctxt src =
    3.36 - (try (fn () => attribute_i (ProofContext.theory_of ctxt) src
    3.37 + (try (fn () => attribute_i (Proof_Context.theory_of ctxt) src
    3.38      (Context.Proof ctxt, Drule.asm_rl)) ();
    3.39    Args.closure src);
    3.40  
    3.41 @@ -185,7 +185,7 @@
    3.42  fun gen_thm pick = Scan.depend (fn context =>
    3.43    let
    3.44      val thy = Context.theory_of context;
    3.45 -    val get = Context.cases (Global_Theory.get_fact context) ProofContext.get_fact context;
    3.46 +    val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
    3.47      val get_fact = get o Facts.Fact;
    3.48      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
    3.49    in
    3.50 @@ -336,7 +336,7 @@
    3.51  
    3.52  fun print_configs ctxt =
    3.53    let
    3.54 -    val thy = ProofContext.theory_of ctxt;
    3.55 +    val thy = Proof_Context.theory_of ctxt;
    3.56      fun prt (name, config) =
    3.57        let val value = Config.get ctxt config in
    3.58          Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
    3.59 @@ -413,7 +413,7 @@
    3.60    register_config Name_Space.short_names_raw #>
    3.61    register_config Name_Space.unique_names_raw #>
    3.62    register_config ML_Context.trace_raw #>
    3.63 -  register_config ProofContext.show_abbrevs_raw #>
    3.64 +  register_config Proof_Context.show_abbrevs_raw #>
    3.65    register_config Goal_Display.goals_limit_raw #>
    3.66    register_config Goal_Display.show_main_goal_raw #>
    3.67    register_config Goal_Display.show_consts_raw #>
     4.1 --- a/src/Pure/Isar/calculation.ML	Sat Apr 16 15:25:25 2011 +0200
     4.2 +++ b/src/Pure/Isar/calculation.ML	Sat Apr 16 15:47:52 2011 +0200
     4.3 @@ -116,8 +116,8 @@
     4.4      val _ =
     4.5        if int then
     4.6          Pretty.writeln
     4.7 -          (ProofContext.pretty_fact ctxt'
     4.8 -            (ProofContext.full_name ctxt' (Binding.name calculationN), calc))
     4.9 +          (Proof_Context.pretty_fact ctxt'
    4.10 +            (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
    4.11        else ();
    4.12    in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
    4.13  
     5.1 --- a/src/Pure/Isar/class.ML	Sat Apr 16 15:25:25 2011 +0200
     5.2 +++ b/src/Pure/Isar/class.ML	Sat Apr 16 15:47:52 2011 +0200
     5.3 @@ -151,7 +151,7 @@
     5.4  
     5.5  fun print_classes ctxt =
     5.6    let
     5.7 -    val thy = ProofContext.theory_of ctxt;
     5.8 +    val thy = Proof_Context.theory_of ctxt;
     5.9      val algebra = Sign.classes_of thy;
    5.10      val arities =
    5.11        Symtab.empty
    5.12 @@ -164,10 +164,10 @@
    5.13          val Ss = Sorts.mg_domain algebra tyco [class];
    5.14        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    5.15      fun mk_param (c, ty) =
    5.16 -      Pretty.str (ProofContext.extern_const ctxt c ^ " :: " ^
    5.17 +      Pretty.str (Proof_Context.extern_const ctxt c ^ " :: " ^
    5.18          Syntax.string_of_typ (Config.put show_sorts false ctxt) (Type.strip_sorts ty));
    5.19      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    5.20 -      (SOME o Pretty.str) ("class " ^ ProofContext.extern_class ctxt class ^ ":"),
    5.21 +      (SOME o Pretty.str) ("class " ^ Proof_Context.extern_class ctxt class ^ ":"),
    5.22        (SOME o Pretty.block) [Pretty.str "supersort: ",
    5.23          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
    5.24        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
    5.25 @@ -257,7 +257,7 @@
    5.26  
    5.27  fun synchronize_class_syntax sort base_sort ctxt =
    5.28    let
    5.29 -    val thy = ProofContext.theory_of ctxt;
    5.30 +    val thy = Proof_Context.theory_of ctxt;
    5.31      val algebra = Sign.classes_of thy;
    5.32      val operations = these_operations thy sort;
    5.33      fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
    5.34 @@ -310,7 +310,7 @@
    5.35    lthy
    5.36    |> Local_Theory.raw_theory f
    5.37    |> Local_Theory.target (synchronize_class_syntax [class]
    5.38 -      (base_sort (ProofContext.theory_of lthy) class));
    5.39 +      (base_sort (Proof_Context.theory_of lthy) class));
    5.40  
    5.41  local
    5.42  
    5.43 @@ -369,10 +369,10 @@
    5.44  fun gen_classrel mk_prop classrel thy =
    5.45    let
    5.46      fun after_qed results =
    5.47 -      ProofContext.background_theory ((fold o fold) AxClass.add_classrel results);
    5.48 +      Proof_Context.background_theory ((fold o fold) AxClass.add_classrel results);
    5.49    in
    5.50      thy
    5.51 -    |> ProofContext.init_global
    5.52 +    |> Proof_Context.init_global
    5.53      |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
    5.54    end;
    5.55  
    5.56 @@ -421,8 +421,8 @@
    5.57  
    5.58  fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
    5.59    let
    5.60 -    val ctxt = ProofContext.init_global thy;
    5.61 -    val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
    5.62 +    val ctxt = Proof_Context.init_global thy;
    5.63 +    val all_arities = map (fn raw_tyco => Proof_Context.read_arity ctxt
    5.64        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    5.65      val tycos = map #1 all_arities;
    5.66      val (_, sorts, sort) = hd all_arities;
    5.67 @@ -437,7 +437,7 @@
    5.68      val Instantiation { params, ... } = Instantiation.get ctxt;
    5.69  
    5.70      val lookup_inst_param = AxClass.lookup_inst_param
    5.71 -      (Sign.consts_of (ProofContext.theory_of ctxt)) params;
    5.72 +      (Sign.consts_of (Proof_Context.theory_of ctxt)) params;
    5.73      fun subst (c, ty) = case lookup_inst_param (c, ty)
    5.74       of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    5.75        | NONE => NONE;
    5.76 @@ -498,23 +498,23 @@
    5.77  fun pretty lthy =
    5.78    let
    5.79      val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
    5.80 -    val thy = ProofContext.theory_of lthy;
    5.81 +    val thy = Proof_Context.theory_of lthy;
    5.82      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    5.83      fun pr_param ((c, _), (v, ty)) =
    5.84        Pretty.block (Pretty.breaks
    5.85 -        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
    5.86 +        [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
    5.87            Pretty.str "::", Syntax.pretty_typ lthy ty]);
    5.88    in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
    5.89  
    5.90  fun conclude lthy =
    5.91    let
    5.92      val (tycos, vs, sort) = #arities (the_instantiation lthy);
    5.93 -    val thy = ProofContext.theory_of lthy;
    5.94 +    val thy = Proof_Context.theory_of lthy;
    5.95      val _ = tycos |> List.app (fn tyco =>
    5.96        if Sign.of_sort thy
    5.97          (Type (tyco, map TFree vs), sort)
    5.98        then ()
    5.99 -      else error ("Missing instance proof for type " ^ quote (ProofContext.extern_type lthy tyco)));
   5.100 +      else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco)));
   5.101    in lthy end;
   5.102  
   5.103  fun instantiation (tycos, vs, sort) thy =
   5.104 @@ -545,7 +545,7 @@
   5.105    in
   5.106      thy
   5.107      |> Theory.checkpoint
   5.108 -    |> ProofContext.init_global
   5.109 +    |> Proof_Context.init_global
   5.110      |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
   5.111      |> fold (Variable.declare_typ o TFree) vs
   5.112      |> fold (Variable.declare_names o Free o snd) params
   5.113 @@ -593,8 +593,8 @@
   5.114  
   5.115  fun prove_instantiation_exit_result f tac x lthy =
   5.116    let
   5.117 -    val morph = ProofContext.export_morphism lthy
   5.118 -      (ProofContext.init_global (ProofContext.theory_of lthy));
   5.119 +    val morph = Proof_Context.export_morphism lthy
   5.120 +      (Proof_Context.init_global (Proof_Context.theory_of lthy));
   5.121      val y = f morph x;
   5.122    in
   5.123      lthy
   5.124 @@ -610,11 +610,11 @@
   5.125      val (tycos, vs, sort) = read_multi_arity thy raw_arities;
   5.126      val sorts = map snd vs;
   5.127      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
   5.128 -    fun after_qed results = ProofContext.background_theory
   5.129 +    fun after_qed results = Proof_Context.background_theory
   5.130        ((fold o fold) AxClass.add_arity results);
   5.131    in
   5.132      thy
   5.133 -    |> ProofContext.init_global
   5.134 +    |> Proof_Context.init_global
   5.135      |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   5.136    end;
   5.137  
     6.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Apr 16 15:25:25 2011 +0200
     6.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Apr 16 15:47:52 2011 +0200
     6.3 @@ -27,7 +27,7 @@
     6.4  
     6.5  fun calculate thy class sups base_sort param_map assm_axiom =
     6.6    let
     6.7 -    val empty_ctxt = ProofContext.init_global thy;
     6.8 +    val empty_ctxt = Proof_Context.init_global thy;
     6.9  
    6.10      (* instantiation of canonical interpretation *)
    6.11      val aT = TFree (Name.aT, base_sort);
    6.12 @@ -55,7 +55,7 @@
    6.13            of (_, NONE) => all_tac
    6.14             | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
    6.15          val tac = loc_intro_tac
    6.16 -          THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
    6.17 +          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom))
    6.18        in Element.prove_witness empty_ctxt prop tac end) prop;
    6.19      val axiom = Option.map Element.conclude_witness wit;
    6.20  
    6.21 @@ -73,7 +73,7 @@
    6.22           of SOME eq_morph => const_morph $> eq_morph
    6.23            | NONE => const_morph
    6.24          val thm'' = Morphism.thm const_eq_morph thm';
    6.25 -        val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
    6.26 +        val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    6.27        in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    6.28      val assm_intro = Option.map prove_assm_intro
    6.29        (fst (Locale.intros_of thy class));
    6.30 @@ -146,11 +146,11 @@
    6.31      (* preprocessing elements, retrieving base sort from type-checked elements *)
    6.32      val raw_supexpr = (map (fn sup => (sup, (("", false),
    6.33        Expression.Positional []))) sups, []);
    6.34 -    val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    6.35 +    val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    6.36        #> Class.redeclare_operations thy sups
    6.37        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    6.38        #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    6.39 -    val ((raw_supparams, _, raw_inferred_elems), _) = ProofContext.init_global thy
    6.40 +    val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
    6.41        |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
    6.42        |> prep_decl raw_supexpr init_class_body raw_elems;
    6.43      fun filter_element (Element.Fixes []) = NONE
    6.44 @@ -207,7 +207,7 @@
    6.45      val sup_sort = inter_sort base_sort sups;
    6.46  
    6.47      (* process elements as class specification *)
    6.48 -    val class_ctxt = Class.begin sups base_sort (ProofContext.init_global thy);
    6.49 +    val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
    6.50      val ((_, _, syntax_elems), _) = class_ctxt
    6.51        |> Expression.cert_declaration supexpr I inferred_elems;
    6.52      fun check_vars e vs = if null vs
    6.53 @@ -324,7 +324,7 @@
    6.54  
    6.55  fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
    6.56    let
    6.57 -    val thy = ProofContext.theory_of lthy;
    6.58 +    val thy = Proof_Context.theory_of lthy;
    6.59      val proto_sup = prep_class thy raw_sup;
    6.60      val proto_sub = case Named_Target.peek lthy
    6.61       of SOME {target, is_class = true, ...} => target
    6.62 @@ -337,9 +337,9 @@
    6.63      val some_prop = try the_single props;
    6.64      val some_dep_morph = try the_single (map snd deps);
    6.65      fun after_qed some_wit =
    6.66 -      ProofContext.background_theory (Class.register_subclass (sub, sup)
    6.67 +      Proof_Context.background_theory (Class.register_subclass (sub, sup)
    6.68          some_dep_morph some_wit export)
    6.69 -      #> ProofContext.theory_of #> Named_Target.init before_exit sub;
    6.70 +      #> Proof_Context.theory_of #> Named_Target.init before_exit sub;
    6.71    in do_proof after_qed some_prop goal_ctxt end;
    6.72  
    6.73  fun user_proof after_qed some_prop =
    6.74 @@ -354,7 +354,7 @@
    6.75  
    6.76  val subclass = gen_subclass (K I) user_proof;
    6.77  fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
    6.78 -val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
    6.79 +val subclass_cmd = gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof;
    6.80  
    6.81  end; (*local*)
    6.82  
     7.1 --- a/src/Pure/Isar/code.ML	Sat Apr 16 15:25:25 2011 +0200
     7.2 +++ b/src/Pure/Isar/code.ML	Sat Apr 16 15:47:52 2011 +0200
     7.3 @@ -113,12 +113,12 @@
     7.4    Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
     7.5  
     7.6  fun string_of_const thy c =
     7.7 -  let val ctxt = ProofContext.init_global thy in
     7.8 +  let val ctxt = Proof_Context.init_global thy in
     7.9      case AxClass.inst_of_param thy c of
    7.10        SOME (c, tyco) =>
    7.11 -        ProofContext.extern_const ctxt c ^ " " ^ enclose "[" "]"
    7.12 -          (ProofContext.extern_type ctxt tyco)
    7.13 -    | NONE => ProofContext.extern_const ctxt c
    7.14 +        Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]"
    7.15 +          (Proof_Context.extern_type ctxt tyco)
    7.16 +    | NONE => Proof_Context.extern_const ctxt c
    7.17    end;
    7.18  
    7.19  
    7.20 @@ -353,7 +353,7 @@
    7.21  fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
    7.22  
    7.23  fun read_signature thy = cert_signature thy o Type.strip_sorts
    7.24 -  o Syntax.parse_typ (ProofContext.init_global thy);
    7.25 +  o Syntax.parse_typ (Proof_Context.init_global thy);
    7.26  
    7.27  fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
    7.28  
    7.29 @@ -576,7 +576,7 @@
    7.30  
    7.31  fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
    7.32  
    7.33 -fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy);
    7.34 +fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
    7.35  
    7.36  fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
    7.37    apfst (meta_rewrite thy);
    7.38 @@ -963,7 +963,7 @@
    7.39  
    7.40  fun print_codesetup thy =
    7.41    let
    7.42 -    val ctxt = ProofContext.init_global thy;
    7.43 +    val ctxt = Proof_Context.init_global thy;
    7.44      val exec = the_exec thy;
    7.45      fun pretty_equations const thms =
    7.46        (Pretty.block o Pretty.fbreaks) (
    7.47 @@ -1150,7 +1150,7 @@
    7.48      fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
    7.49      val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
    7.50      fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
    7.51 -      THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
    7.52 +      THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
    7.53    in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
    7.54  
    7.55  fun add_case thm thy =
     8.1 --- a/src/Pure/Isar/element.ML	Sat Apr 16 15:25:25 2011 +0200
     8.2 +++ b/src/Pure/Isar/element.ML	Sat Apr 16 15:47:52 2011 +0200
     8.3 @@ -222,7 +222,7 @@
     8.4  fun obtain prop ctxt =
     8.5    let
     8.6      val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
     8.7 -    fun fix (x, T) = (Binding.name (ProofContext.revert_skolem ctxt' x), SOME T);
     8.8 +    fun fix (x, T) = (Binding.name (Proof_Context.revert_skolem ctxt' x), SOME T);
     8.9      val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
    8.10      val As = Logic.strip_imp_prems (Thm.term_of prop');
    8.11    in ((Binding.empty, (xs, As)), ctxt') end;
    8.12 @@ -231,7 +231,7 @@
    8.13  
    8.14  fun pretty_statement ctxt kind raw_th =
    8.15    let
    8.16 -    val thy = ProofContext.theory_of ctxt;
    8.17 +    val thy = Proof_Context.theory_of ctxt;
    8.18      val cert = Thm.cterm_of thy;
    8.19  
    8.20      val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
    8.21 @@ -242,7 +242,7 @@
    8.22  
    8.23      val fixes = fold_aterms (fn v as Free (x, T) =>
    8.24          if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
    8.25 -        then insert (op =) (ProofContext.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
    8.26 +        then insert (op =) (Proof_Context.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
    8.27      val (assumes, cases) = take_suffix (fn prem =>
    8.28        is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
    8.29    in
    8.30 @@ -295,7 +295,7 @@
    8.31  
    8.32  fun proof_local cmd goal_ctxt int after_qed' propss =
    8.33      Proof.map_context (K goal_ctxt)
    8.34 -    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
    8.35 +    #> Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
    8.36        cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
    8.37  
    8.38  in
    8.39 @@ -491,27 +491,27 @@
    8.40    in
    8.41      context |> Context.mapping_result
    8.42        (Global_Theory.note_thmss kind facts')
    8.43 -      (ProofContext.note_thmss kind facts')
    8.44 +      (Proof_Context.note_thmss kind facts')
    8.45    end;
    8.46  
    8.47 -fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
    8.48 +fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
    8.49    | init (Constrains _) = I
    8.50    | init (Assumes asms) = Context.map_proof (fn ctxt =>
    8.51        let
    8.52 -        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
    8.53 +        val asms' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) asms;
    8.54          val (_, ctxt') = ctxt
    8.55            |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
    8.56 -          |> ProofContext.add_assms_i Assumption.assume_export asms';
    8.57 +          |> Proof_Context.add_assms_i Assumption.assume_export asms';
    8.58        in ctxt' end)
    8.59    | init (Defines defs) = Context.map_proof (fn ctxt =>
    8.60        let
    8.61 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    8.62 +        val defs' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) defs;
    8.63          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    8.64              let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
    8.65              in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
    8.66          val (_, ctxt') = ctxt
    8.67            |> fold Variable.auto_fixes (map #1 asms)
    8.68 -          |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
    8.69 +          |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
    8.70        in ctxt' end)
    8.71    | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
    8.72  
    8.73 @@ -530,8 +530,8 @@
    8.74      typ = I,
    8.75      term = I,
    8.76      pattern = I,
    8.77 -    fact = ProofContext.get_fact ctxt,
    8.78 -    attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}
    8.79 +    fact = Proof_Context.get_fact ctxt,
    8.80 +    attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)}
    8.81    in activate_i elem ctxt end;
    8.82  
    8.83  end;
     9.1 --- a/src/Pure/Isar/expression.ML	Sat Apr 16 15:25:25 2011 +0200
     9.2 +++ b/src/Pure/Isar/expression.ML	Sat Apr 16 15:47:52 2011 +0200
     9.3 @@ -185,7 +185,7 @@
     9.4      val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
     9.5      val inst = Symtab.make insts'';
     9.6    in
     9.7 -    (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
     9.8 +    (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
     9.9        Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
    9.10    end;
    9.11  
    9.12 @@ -198,15 +198,15 @@
    9.13    Element.map_ctxt
    9.14     {binding = I,
    9.15      typ = prep_typ ctxt,
    9.16 -    term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt),
    9.17 -    pattern = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
    9.18 +    term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt),
    9.19 +    pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt),
    9.20      fact = I,
    9.21      attrib = I};
    9.22  
    9.23  fun parse_concl prep_term ctxt concl =
    9.24    (map o map) (fn (t, ps) =>
    9.25 -    (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t,
    9.26 -      map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
    9.27 +    (prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
    9.28 +      map (prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) concl;
    9.29  
    9.30  
    9.31  (** Simultaneous type inference: instantiations + elements + conclusion **)
    9.32 @@ -247,12 +247,12 @@
    9.33      fun prep (_, pats) (ctxt, t :: ts) =
    9.34        let val ctxt' = Variable.auto_fixes t ctxt
    9.35        in
    9.36 -        ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
    9.37 +        ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
    9.38            (ctxt', ts))
    9.39        end;
    9.40      val (cs', (context', _)) = fold_map prep cs
    9.41        (context, Syntax.check_terms
    9.42 -        (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
    9.43 +        (Proof_Context.set_mode Proof_Context.mode_schematic context) (map fst cs));
    9.44    in (cs', context') end;
    9.45  
    9.46  in
    9.47 @@ -279,7 +279,7 @@
    9.48  
    9.49  fun declare_elem prep_vars (Fixes fixes) ctxt =
    9.50        let val (vars, _) = prep_vars fixes ctxt
    9.51 -      in ctxt |> ProofContext.add_fixes vars |> snd end
    9.52 +      in ctxt |> Proof_Context.add_fixes vars |> snd end
    9.53    | declare_elem prep_vars (Constrains csts) ctxt =
    9.54        ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
    9.55    | declare_elem _ (Assumes _) ctxt = ctxt
    9.56 @@ -322,7 +322,7 @@
    9.57  
    9.58  fun finish_inst ctxt (loc, (prfx, inst)) =
    9.59    let
    9.60 -    val thy = ProofContext.theory_of ctxt;
    9.61 +    val thy = Proof_Context.theory_of ctxt;
    9.62      val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    9.63      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
    9.64    in (loc, morph) end;
    9.65 @@ -346,7 +346,7 @@
    9.66  fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
    9.67      {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
    9.68    let
    9.69 -    val thy = ProofContext.theory_of ctxt1;
    9.70 +    val thy = Proof_Context.theory_of ctxt1;
    9.71  
    9.72      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
    9.73  
    9.74 @@ -377,7 +377,7 @@
    9.75        in check_autofix insts elems concl ctxt end;
    9.76  
    9.77      val fors = prep_vars_inst fixed ctxt1 |> fst;
    9.78 -    val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
    9.79 +    val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
    9.80      val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
    9.81  
    9.82      val add_free = fold_aterms
    9.83 @@ -397,7 +397,7 @@
    9.84      (* Retrieve parameter types *)
    9.85      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
    9.86        | _ => fn ps => ps) (Fixes fors :: elems') [];
    9.87 -    val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
    9.88 +    val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
    9.89      val parms = xs ~~ Ts;  (* params from expression and elements *)
    9.90  
    9.91      val Fixes fors' = finish_primitive parms I (Fixes fors);
    9.92 @@ -409,16 +409,16 @@
    9.93  in
    9.94  
    9.95  fun cert_full_context_statement x =
    9.96 -  prep_full_context_statement (K I) (K I) ProofContext.cert_vars
    9.97 -  make_inst ProofContext.cert_vars (K I) x;
    9.98 +  prep_full_context_statement (K I) (K I) Proof_Context.cert_vars
    9.99 +  make_inst Proof_Context.cert_vars (K I) x;
   9.100  
   9.101  fun cert_read_full_context_statement x =
   9.102 -  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   9.103 -  make_inst ProofContext.cert_vars (K I) x;
   9.104 +  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
   9.105 +  make_inst Proof_Context.cert_vars (K I) x;
   9.106  
   9.107  fun read_full_context_statement x =
   9.108 -  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
   9.109 -  parse_inst ProofContext.read_vars intern x;
   9.110 +  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
   9.111 +  parse_inst Proof_Context.read_vars intern x;
   9.112  
   9.113  end;
   9.114  
   9.115 @@ -433,7 +433,7 @@
   9.116         prep {strict = true, do_close = false, fixed_frees = true}
   9.117          ([], []) I raw_elems raw_concl context;
   9.118       val (_, context') = context |>
   9.119 -       ProofContext.set_stmt true |>
   9.120 +       Proof_Context.set_stmt true |>
   9.121         fold_map activate elems;
   9.122    in (concl, context') end;
   9.123  
   9.124 @@ -448,7 +448,7 @@
   9.125  (* Locale declaration: import + elements *)
   9.126  
   9.127  fun fix_params params =
   9.128 -  ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
   9.129 +  Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
   9.130  
   9.131  local
   9.132  
   9.133 @@ -462,7 +462,7 @@
   9.134        fix_params fixed |>
   9.135        fold (Context.proof_map o Locale.activate_facts NONE) deps;
   9.136      val (elems', _) = context' |>
   9.137 -      ProofContext.set_stmt true |>
   9.138 +      Proof_Context.set_stmt true |>
   9.139        fold_map activate elems;
   9.140    in ((fixed, deps, elems'), (parms, ctxt')) end;
   9.141  
   9.142 @@ -488,7 +488,7 @@
   9.143  
   9.144  fun prep_goal_expression prep expression context =
   9.145    let
   9.146 -    val thy = ProofContext.theory_of context;
   9.147 +    val thy = Proof_Context.theory_of context;
   9.148  
   9.149      val ((fixed, deps, _, _), _) =
   9.150        prep {strict = true, do_close = true, fixed_frees = true} expression I [] [] context;
   9.151 @@ -566,7 +566,7 @@
   9.152  
   9.153  fun eval_inst ctxt (loc, morph) text =
   9.154    let
   9.155 -    val thy = ProofContext.theory_of ctxt;
   9.156 +    val thy = Proof_Context.theory_of ctxt;
   9.157      val (asm, defs) = Locale.specification_of thy loc;
   9.158      val asm' = Option.map (Morphism.term morph) asm;
   9.159      val defs' = map (Morphism.term morph) defs;
   9.160 @@ -616,7 +616,7 @@
   9.161  fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
   9.162    if length args = n then
   9.163      Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
   9.164 -      Term.list_comb (Syntax.free (ProofContext.extern_const ctxt c), args)
   9.165 +      Term.list_comb (Syntax.free (Proof_Context.extern_const ctxt c), args)
   9.166    else raise Match);
   9.167  
   9.168  (* define one predicate including its intro rule and axioms
   9.169 @@ -651,7 +651,7 @@
   9.170        |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
   9.171        |> Global_Theory.add_defs false
   9.172          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
   9.173 -    val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
   9.174 +    val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
   9.175  
   9.176      val cert = Thm.cterm_of defs_thy;
   9.177  
   9.178 @@ -738,7 +738,7 @@
   9.179        error ("Duplicate definition of locale " ^ quote name);
   9.180  
   9.181      val ((fixed, deps, body_elems), (parms, ctxt')) =
   9.182 -      prep_decl raw_import I raw_body (ProofContext.init_global thy);
   9.183 +      prep_decl raw_import I raw_body (Proof_Context.init_global thy);
   9.184      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
   9.185  
   9.186      val extraTs =
   9.187 @@ -825,7 +825,7 @@
   9.188  fun gen_interpretation prep_expr parse_prop prep_attr
   9.189      expression equations theory =
   9.190    let
   9.191 -    val ((propss, deps, export), expr_ctxt) = ProofContext.init_global theory
   9.192 +    val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
   9.193        |> prep_expr expression;
   9.194  
   9.195      val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
   9.196 @@ -834,7 +834,7 @@
   9.197      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   9.198  
   9.199      fun after_qed witss eqns =
   9.200 -      (ProofContext.background_theory o Context.theory_map)
   9.201 +      (Proof_Context.background_theory o Context.theory_map)
   9.202          (note_eqns_register deps witss attrss eqns export export');
   9.203  
   9.204    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
   9.205 @@ -844,7 +844,7 @@
   9.206    let
   9.207      val _ = Proof.assert_forward_or_chain state;
   9.208      val ctxt = Proof.context_of state;
   9.209 -    val theory = ProofContext.theory_of ctxt;
   9.210 +    val theory = Proof_Context.theory_of ctxt;
   9.211  
   9.212      val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
   9.213  
   9.214 @@ -891,7 +891,7 @@
   9.215    in
   9.216      ctxt
   9.217      |> Locale.add_thmss target Thm.lemmaK facts
   9.218 -    |> ProofContext.background_theory (fold (fn ((dep, morph), wits) =>
   9.219 +    |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
   9.220        fn theory =>
   9.221          Locale.add_dependency target
   9.222            (dep, morph $> Element.satisfy_morphism
    10.1 --- a/src/Pure/Isar/generic_target.ML	Sat Apr 16 15:25:25 2011 +0200
    10.2 +++ b/src/Pure/Isar/generic_target.ML	Sat Apr 16 15:47:52 2011 +0200
    10.3 @@ -50,8 +50,8 @@
    10.4  
    10.5  fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
    10.6    let
    10.7 -    val thy = ProofContext.theory_of lthy;
    10.8 -    val thy_ctxt = ProofContext.init_global thy;
    10.9 +    val thy = Proof_Context.theory_of lthy;
   10.10 +    val thy_ctxt = Proof_Context.init_global thy;
   10.11  
   10.12      val b_def = Thm.def_binding_optional b proto_b_def;
   10.13  
   10.14 @@ -99,8 +99,8 @@
   10.15  
   10.16  fun import_export_proof ctxt (name, raw_th) =
   10.17    let
   10.18 -    val thy = ProofContext.theory_of ctxt;
   10.19 -    val thy_ctxt = ProofContext.init_global thy;
   10.20 +    val thy = Proof_Context.theory_of ctxt;
   10.21 +    val thy_ctxt = Proof_Context.init_global thy;
   10.22      val certT = Thm.ctyp_of thy;
   10.23      val cert = Thm.cterm_of thy;
   10.24  
   10.25 @@ -145,7 +145,7 @@
   10.26  
   10.27  fun notes target_notes kind facts lthy =
   10.28    let
   10.29 -    val thy = ProofContext.theory_of lthy;
   10.30 +    val thy = Proof_Context.theory_of lthy;
   10.31      val facts' = facts
   10.32        |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
   10.33            (Local_Theory.full_name lthy (fst a))) bs))
   10.34 @@ -155,7 +155,7 @@
   10.35    in
   10.36      lthy
   10.37      |> target_notes kind global_facts local_facts
   10.38 -    |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
   10.39 +    |> Proof_Context.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
   10.40    end;
   10.41  
   10.42  
   10.43 @@ -163,7 +163,7 @@
   10.44  
   10.45  fun abbrev target_abbrev prmode ((b, mx), t) lthy =
   10.46    let
   10.47 -    val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
   10.48 +    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
   10.49      val target_ctxt = Local_Theory.target_of lthy;
   10.50  
   10.51      val t' = Assumption.export_term lthy target_ctxt t;
   10.52 @@ -179,7 +179,7 @@
   10.53    in
   10.54      lthy
   10.55      |> target_abbrev prmode (b, mx') (global_rhs, t') xs
   10.56 -    |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
   10.57 +    |> Proof_Context.add_abbrev Print_Mode.internal (b, t) |> snd
   10.58      |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
   10.59    end;
   10.60  
   10.61 @@ -207,12 +207,12 @@
   10.62  
   10.63  fun theory_notes kind global_facts lthy =
   10.64    let
   10.65 -    val thy = ProofContext.theory_of lthy;
   10.66 +    val thy = Proof_Context.theory_of lthy;
   10.67      val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
   10.68    in
   10.69      lthy
   10.70      |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
   10.71 -    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
   10.72 +    |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
   10.73    end;
   10.74  
   10.75  fun theory_abbrev prmode ((b, mx), t) =
    11.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 15:25:25 2011 +0200
    11.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 15:47:52 2011 +0200
    11.3 @@ -159,10 +159,10 @@
    11.4  
    11.5  fun read_trrules thy raw_rules =
    11.6    let
    11.7 -    val ctxt = ProofContext.init_global thy;
    11.8 +    val ctxt = Proof_Context.init_global thy;
    11.9    in
   11.10      raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
   11.11 -      Syntax_Phases.parse_ast_pattern ctxt (ProofContext.intern_type ctxt r, s)))
   11.12 +      Syntax_Phases.parse_ast_pattern ctxt (Proof_Context.intern_type ctxt r, s)))
   11.13    end;
   11.14  
   11.15  fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
   11.16 @@ -326,24 +326,24 @@
   11.17    Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
   11.18  
   11.19  val print_syntax = Toplevel.unknown_context o
   11.20 -  Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
   11.21 +  Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of);
   11.22  
   11.23  val print_abbrevs = Toplevel.unknown_context o
   11.24 -  Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
   11.25 +  Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of);
   11.26  
   11.27  val print_facts = Toplevel.unknown_context o
   11.28 -  Toplevel.keep (ProofContext.print_lthms o Toplevel.context_of);
   11.29 +  Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of);
   11.30  
   11.31  val print_configs = Toplevel.unknown_context o
   11.32    Toplevel.keep (Attrib.print_configs o Toplevel.context_of);
   11.33  
   11.34  val print_theorems_proof =
   11.35 -  Toplevel.keep (ProofContext.print_lthms o Proof.context_of o Toplevel.proof_of);
   11.36 +  Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);
   11.37  
   11.38  fun print_theorems_theory verbose = Toplevel.keep (fn state =>
   11.39    Toplevel.theory_of state |>
   11.40    (case Toplevel.previous_context_of state of
   11.41 -    SOME prev => Proof_Display.print_theorems_diff verbose (ProofContext.theory_of prev)
   11.42 +    SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev)
   11.43    | NONE => Proof_Display.print_theorems verbose));
   11.44  
   11.45  fun print_theorems verbose =
   11.46 @@ -400,7 +400,7 @@
   11.47  val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   11.48    let
   11.49      val ctxt = Toplevel.context_of state;
   11.50 -    val {classes = (space, algebra), ...} = Type.rep_tsig (ProofContext.tsig_of ctxt);
   11.51 +    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
   11.52      val classes = Sorts.classes_of algebra;
   11.53      fun entry (c, (i, (_, cs))) =
   11.54        (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
   11.55 @@ -421,7 +421,7 @@
   11.56    let
   11.57      val thy = Toplevel.theory_of state;
   11.58      val ctxt = Toplevel.context_of state;
   11.59 -    fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
   11.60 +    fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
   11.61      val get_theory = Context.get_theory thy;
   11.62    in
   11.63      Thm_Deps.unused_thms
   11.64 @@ -436,10 +436,10 @@
   11.65  (* print proof context contents *)
   11.66  
   11.67  val print_binds = Toplevel.unknown_context o
   11.68 -  Toplevel.keep (ProofContext.print_binds o Toplevel.context_of);
   11.69 +  Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of);
   11.70  
   11.71  val print_cases = Toplevel.unknown_context o
   11.72 -  Toplevel.keep (ProofContext.print_cases o Toplevel.context_of);
   11.73 +  Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of);
   11.74  
   11.75  
   11.76  (* print theorems, terms, types etc. *)
   11.77 @@ -460,7 +460,7 @@
   11.78        NONE =>
   11.79          let
   11.80            val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
   11.81 -          val thy = ProofContext.theory_of ctxt;
   11.82 +          val thy = Proof_Context.theory_of ctxt;
   11.83            val prf = Thm.proof_of thm;
   11.84            val prop = Thm.full_prop_of thm;
   11.85            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
    12.1 --- a/src/Pure/Isar/local_defs.ML	Sat Apr 16 15:25:25 2011 +0200
    12.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Apr 16 15:47:52 2011 +0200
    12.3 @@ -58,7 +58,7 @@
    12.4  fun mk_def ctxt args =
    12.5    let
    12.6      val (xs, rhss) = split_list args;
    12.7 -    val (bind, _) = ProofContext.bind_fixes xs ctxt;
    12.8 +    val (bind, _) = Proof_Context.bind_fixes xs ctxt;
    12.9      val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
   12.10    in map Logic.mk_equals (lhss ~~ rhss) end;
   12.11  
   12.12 @@ -98,9 +98,9 @@
   12.13      val lhss = map (fst o Logic.dest_equals) eqs;
   12.14    in
   12.15      ctxt
   12.16 -    |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
   12.17 +    |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
   12.18      |> fold Variable.declare_term eqs
   12.19 -    |> ProofContext.add_assms_i def_export
   12.20 +    |> Proof_Context.add_assms_i def_export
   12.21        (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
   12.22      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   12.23    end;
   12.24 @@ -117,7 +117,7 @@
   12.25      val T = Term.fastype_of rhs;
   12.26      val ([x'], ctxt') = ctxt
   12.27        |> Variable.declare_term rhs
   12.28 -      |> ProofContext.add_fixes [(x, SOME T, mx)];
   12.29 +      |> Proof_Context.add_fixes [(x, SOME T, mx)];
   12.30      val lhs = Free (x', T);
   12.31      val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
   12.32      fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
   12.33 @@ -232,7 +232,7 @@
   12.34  fun derived_def ctxt conditional prop =
   12.35    let
   12.36      val ((c, T), rhs) = prop
   12.37 -      |> Thm.cterm_of (ProofContext.theory_of ctxt)
   12.38 +      |> Thm.cterm_of (Proof_Context.theory_of ctxt)
   12.39        |> meta_rewrite_conv ctxt
   12.40        |> (snd o Logic.dest_equals o Thm.prop_of)
   12.41        |> conditional ? Logic.strip_imp_concl
    13.1 --- a/src/Pure/Isar/local_theory.ML	Sat Apr 16 15:25:25 2011 +0200
    13.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Apr 16 15:47:52 2011 +0200
    13.3 @@ -134,10 +134,10 @@
    13.4  
    13.5  fun raw_theory_result f lthy =
    13.6    let
    13.7 -    val (res, thy') = f (ProofContext.theory_of lthy);
    13.8 +    val (res, thy') = f (Proof_Context.theory_of lthy);
    13.9      val lthy' = lthy
   13.10 -      |> map_target (ProofContext.transfer thy')
   13.11 -      |> ProofContext.transfer thy';
   13.12 +      |> map_target (Proof_Context.transfer thy')
   13.13 +      |> Proof_Context.transfer thy';
   13.14    in (res, lthy') end;
   13.15  
   13.16  fun raw_theory f = #2 o raw_theory_result (f #> pair ());
   13.17 @@ -160,10 +160,10 @@
   13.18        |> Context_Position.set_visible false
   13.19        |> f
   13.20        ||> Context_Position.restore_visible lthy;
   13.21 -    val thy' = ProofContext.theory_of ctxt';
   13.22 +    val thy' = Proof_Context.theory_of ctxt';
   13.23      val lthy' = lthy
   13.24        |> map_target (K ctxt')
   13.25 -      |> ProofContext.transfer thy';
   13.26 +      |> Proof_Context.transfer thy';
   13.27    in (res, lthy') end;
   13.28  
   13.29  fun target f = #2 o target_result (f #> pair ());
   13.30 @@ -181,12 +181,12 @@
   13.31  (* morphisms *)
   13.32  
   13.33  fun standard_morphism lthy ctxt =
   13.34 -  ProofContext.norm_export_morphism lthy ctxt $>
   13.35 +  Proof_Context.norm_export_morphism lthy ctxt $>
   13.36    Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
   13.37  
   13.38  fun target_morphism lthy = standard_morphism lthy (target_of lthy);
   13.39  fun global_morphism lthy =
   13.40 -  standard_morphism lthy (ProofContext.init_global (ProofContext.theory_of lthy));
   13.41 +  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
   13.42  
   13.43  
   13.44  (* primitive operations *)
   13.45 @@ -210,18 +210,18 @@
   13.46  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
   13.47  
   13.48  fun set_defsort S =
   13.49 -  syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (ProofContext.set_defsort S)));
   13.50 +  syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
   13.51  
   13.52  
   13.53  (* notation *)
   13.54  
   13.55  fun type_notation add mode raw_args lthy =
   13.56    let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
   13.57 -  in syntax_declaration false (ProofContext.target_type_notation add mode args) lthy end;
   13.58 +  in syntax_declaration false (Proof_Context.target_type_notation add mode args) lthy end;
   13.59  
   13.60  fun notation add mode raw_args lthy =
   13.61    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   13.62 -  in syntax_declaration false (ProofContext.target_notation add mode args) lthy end;
   13.63 +  in syntax_declaration false (Proof_Context.target_notation add mode args) lthy end;
   13.64  
   13.65  
   13.66  (* name space aliases *)
   13.67 @@ -232,9 +232,9 @@
   13.68      in Context.mapping (global_alias b' name) (local_alias b' name) end)
   13.69    #> local_alias b name;
   13.70  
   13.71 -val class_alias = alias Sign.class_alias ProofContext.class_alias;
   13.72 -val type_alias = alias Sign.type_alias ProofContext.type_alias;
   13.73 -val const_alias = alias Sign.const_alias ProofContext.const_alias;
   13.74 +val class_alias = alias Sign.class_alias Proof_Context.class_alias;
   13.75 +val type_alias = alias Sign.type_alias Proof_Context.type_alias;
   13.76 +val const_alias = alias Sign.const_alias Proof_Context.const_alias;
   13.77  
   13.78  
   13.79  
   13.80 @@ -244,7 +244,7 @@
   13.81  
   13.82  fun init group theory_prefix operations target =
   13.83    let val naming =
   13.84 -    Sign.naming_of (ProofContext.theory_of target)
   13.85 +    Sign.naming_of (Proof_Context.theory_of target)
   13.86      |> Name_Space.set_group group
   13.87      |> Name_Space.mandatory_path theory_prefix;
   13.88    in
   13.89 @@ -261,8 +261,8 @@
   13.90  
   13.91  (* exit *)
   13.92  
   13.93 -val exit = ProofContext.background_theory Theory.checkpoint o operation #exit;
   13.94 -val exit_global = ProofContext.theory_of o exit;
   13.95 +val exit = Proof_Context.background_theory Theory.checkpoint o operation #exit;
   13.96 +val exit_global = Proof_Context.theory_of o exit;
   13.97  
   13.98  fun exit_result f (x, lthy) =
   13.99    let
  13.100 @@ -273,7 +273,7 @@
  13.101  fun exit_result_global f (x, lthy) =
  13.102    let
  13.103      val thy = exit_global lthy;
  13.104 -    val thy_ctxt = ProofContext.init_global thy;
  13.105 +    val thy_ctxt = Proof_Context.init_global thy;
  13.106      val phi = standard_morphism lthy thy_ctxt;
  13.107    in (f phi x, thy) end;
  13.108  
    14.1 --- a/src/Pure/Isar/locale.ML	Sat Apr 16 15:25:25 2011 +0200
    14.2 +++ b/src/Pure/Isar/locale.ML	Sat Apr 16 15:47:52 2011 +0200
    14.3 @@ -162,7 +162,7 @@
    14.4  );
    14.5  
    14.6  val intern = Name_Space.intern o #1 o Locales.get;
    14.7 -fun extern thy = Name_Space.extern (ProofContext.init_global thy) (#1 (Locales.get thy));
    14.8 +fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
    14.9  
   14.10  val get_locale = Symtab.lookup o #2 o Locales.get;
   14.11  val defined = Symtab.defined o #2 o Locales.get;
   14.12 @@ -215,7 +215,7 @@
   14.13  
   14.14  fun pretty_reg ctxt (name, morph) =
   14.15    let
   14.16 -    val thy = ProofContext.theory_of ctxt;
   14.17 +    val thy = Proof_Context.theory_of ctxt;
   14.18      val name' = extern thy name;
   14.19      fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   14.20      fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   14.21 @@ -469,7 +469,7 @@
   14.22  
   14.23  fun init name thy =
   14.24    activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
   14.25 -    ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
   14.26 +    ([], Context.Proof (Proof_Context.init_global thy)) |-> put_idents |> Context.proof_of;
   14.27  
   14.28  
   14.29  (*** Add and extend registrations ***)
   14.30 @@ -556,7 +556,7 @@
   14.31  fun add_thmss loc kind args ctxt =
   14.32    let
   14.33      val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
   14.34 -    val ctxt'' = ctxt' |> ProofContext.background_theory
   14.35 +    val ctxt'' = ctxt' |> Proof_Context.background_theory
   14.36       ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
   14.37          #>
   14.38        (* Registrations *)
   14.39 @@ -578,7 +578,7 @@
   14.40        [([Drule.dummy_thm], [])])];
   14.41  
   14.42  fun add_syntax_declaration loc decl =
   14.43 -  ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   14.44 +  Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   14.45    #> add_declaration loc decl;
   14.46  
   14.47  
   14.48 @@ -631,7 +631,7 @@
   14.49  
   14.50  fun print_locales thy =
   14.51    Pretty.strs ("locales:" ::
   14.52 -    map #1 (Name_Space.extern_table (ProofContext.init_global thy) (Locales.get thy)))
   14.53 +    map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
   14.54    |> Pretty.writeln;
   14.55  
   14.56  fun print_locale thy show_facts raw_name =
   14.57 @@ -650,7 +650,7 @@
   14.58  
   14.59  fun print_registrations ctxt raw_name =
   14.60    let
   14.61 -    val thy = ProofContext.theory_of ctxt;
   14.62 +    val thy = Proof_Context.theory_of ctxt;
   14.63      val name = intern thy raw_name;
   14.64      val _ = the_locale thy name;  (* error if locale unknown *)
   14.65    in
   14.66 @@ -661,7 +661,7 @@
   14.67  
   14.68  fun print_dependencies ctxt clean export insts =
   14.69    let
   14.70 -    val thy = ProofContext.theory_of ctxt;
   14.71 +    val thy = Proof_Context.theory_of ctxt;
   14.72      val idents = if clean then [] else get_idents (Context.Proof ctxt);
   14.73    in
   14.74      (case fold (roundup thy cons export) insts (idents, []) |> snd of
    15.1 --- a/src/Pure/Isar/method.ML	Sat Apr 16 15:25:25 2011 +0200
    15.2 +++ b/src/Pure/Isar/method.ML	Sat Apr 16 15:47:52 2011 +0200
    15.3 @@ -154,7 +154,7 @@
    15.4  
    15.5  fun cheating int ctxt =
    15.6    if int orelse ! quick_and_dirty then
    15.7 -    METHOD (K (Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)))
    15.8 +    METHOD (K (Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)))
    15.9    else error "Cheating requires quick_and_dirty mode!";
   15.10  
   15.11  
   15.12 @@ -183,8 +183,8 @@
   15.13  
   15.14  (* fact -- composition by facts from context *)
   15.15  
   15.16 -fun fact [] ctxt = SIMPLE_METHOD' (ProofContext.some_fact_tac ctxt)
   15.17 -  | fact rules _ = SIMPLE_METHOD' (ProofContext.fact_tac rules);
   15.18 +fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
   15.19 +  | fact rules _ = SIMPLE_METHOD' (Proof_Context.fact_tac rules);
   15.20  
   15.21  
   15.22  (* assumption *)
   15.23 @@ -334,7 +334,7 @@
   15.24  
   15.25  fun print_methods thy =
   15.26    let
   15.27 -    val ctxt = ProofContext.init_global thy;
   15.28 +    val ctxt = Proof_Context.init_global thy;
   15.29      val meths = Methods.get thy;
   15.30      fun prt_meth (name, (_, comment)) = Pretty.block
   15.31        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    16.1 --- a/src/Pure/Isar/named_target.ML	Sat Apr 16 15:25:25 2011 +0200
    16.2 +++ b/src/Pure/Isar/named_target.ML	Sat Apr 16 15:47:52 2011 +0200
    16.3 @@ -80,12 +80,12 @@
    16.4      not is_canonical_class ?
    16.5        (Context.mapping_result
    16.6          (Sign.add_abbrev Print_Mode.internal arg)
    16.7 -        (ProofContext.add_abbrev Print_Mode.internal arg)
    16.8 +        (Proof_Context.add_abbrev Print_Mode.internal arg)
    16.9        #-> (fn (lhs' as Const (d, _), _) =>
   16.10            same_shape ?
   16.11              (Context.mapping
   16.12 -              (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
   16.13 -             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   16.14 +              (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
   16.15 +             Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
   16.16    end;
   16.17  
   16.18  fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
   16.19 @@ -153,12 +153,12 @@
   16.20  
   16.21  fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
   16.22    let
   16.23 -    val thy = ProofContext.theory_of ctxt;
   16.24 +    val thy = Proof_Context.theory_of ctxt;
   16.25      val target_name =
   16.26        [Pretty.command (if is_class then "class" else "locale"),
   16.27          Pretty.str (" " ^ Locale.extern thy target)];
   16.28      val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
   16.29 -      (#1 (ProofContext.inferred_fixes ctxt));
   16.30 +      (#1 (Proof_Context.inferred_fixes ctxt));
   16.31      val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
   16.32        (Assumption.all_assms_of ctxt);
   16.33      val elems =
   16.34 @@ -171,14 +171,14 @@
   16.35          map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
   16.36    in
   16.37      Pretty.block [Pretty.command "theory", Pretty.brk 1,
   16.38 -      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
   16.39 +      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
   16.40    end;
   16.41  
   16.42  
   16.43  (* init *)
   16.44  
   16.45  fun init_context (Target {target, is_locale, is_class, ...}) =
   16.46 -  if not is_locale then ProofContext.init_global
   16.47 +  if not is_locale then Proof_Context.init_global
   16.48    else if not is_class then Locale.init target
   16.49    else Class.init target;
   16.50  
    17.1 --- a/src/Pure/Isar/object_logic.ML	Sat Apr 16 15:25:25 2011 +0200
    17.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Apr 16 15:47:52 2011 +0200
    17.3 @@ -188,7 +188,7 @@
    17.4  fun atomize_prems ct =
    17.5    if Logic.has_meta_prems (Thm.term_of ct) then
    17.6      Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
    17.7 -      (ProofContext.init_global (Thm.theory_of_cterm ct)) ct
    17.8 +      (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
    17.9    else Conv.all_conv ct;
   17.10  
   17.11  val atomize_prems_tac = CONVERSION atomize_prems;
    18.1 --- a/src/Pure/Isar/obtain.ML	Sat Apr 16 15:25:25 2011 +0200
    18.2 +++ b/src/Pure/Isar/obtain.ML	Sat Apr 16 15:47:52 2011 +0200
    18.3 @@ -73,7 +73,7 @@
    18.4  
    18.5  fun eliminate fix_ctxt rule xs As thm =
    18.6    let
    18.7 -    val thy = ProofContext.theory_of fix_ctxt;
    18.8 +    val thy = Proof_Context.theory_of fix_ctxt;
    18.9  
   18.10      val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
   18.11      val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
   18.12 @@ -99,8 +99,8 @@
   18.13  
   18.14  fun bind_judgment ctxt name =
   18.15    let
   18.16 -    val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
   18.17 -    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
   18.18 +    val (bind, ctxt') = Proof_Context.bind_fixes [name] ctxt;
   18.19 +    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name);
   18.20    in ((v, t), ctxt') end;
   18.21  
   18.22  val thatN = "that";
   18.23 @@ -118,7 +118,7 @@
   18.24  
   18.25      (*obtain vars*)
   18.26      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
   18.27 -    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
   18.28 +    val (_, fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
   18.29      val xs = map (Variable.name o #1) vars;
   18.30  
   18.31      (*obtain asms*)
   18.32 @@ -134,7 +134,7 @@
   18.33  
   18.34      val asm_frees = fold Term.add_frees asm_props [];
   18.35      val parms = xs |> map (fn x =>
   18.36 -      let val x' = ProofContext.get_skolem fix_ctxt x
   18.37 +      let val x' = Proof_Context.get_skolem fix_ctxt x
   18.38        in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
   18.39  
   18.40      val that_name = if name = "" then thatN else name;
   18.41 @@ -166,8 +166,8 @@
   18.42  
   18.43  in
   18.44  
   18.45 -val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
   18.46 -val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
   18.47 +val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
   18.48 +val obtain_cmd = gen_obtain Attrib.attribute Proof_Context.read_vars Proof_Context.read_propp;
   18.49  
   18.50  end;
   18.51  
   18.52 @@ -186,7 +186,7 @@
   18.53  
   18.54  fun result tac facts ctxt =
   18.55    let
   18.56 -    val thy = ProofContext.theory_of ctxt;
   18.57 +    val thy = Proof_Context.theory_of ctxt;
   18.58      val cert = Thm.cterm_of thy;
   18.59  
   18.60      val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
   18.61 @@ -212,7 +212,7 @@
   18.62  
   18.63  fun unify_params vars thesis_var raw_rule ctxt =
   18.64    let
   18.65 -    val thy = ProofContext.theory_of ctxt;
   18.66 +    val thy = Proof_Context.theory_of ctxt;
   18.67      val certT = Thm.ctyp_of thy;
   18.68      val cert = Thm.cterm_of thy;
   18.69      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
   18.70 @@ -258,7 +258,7 @@
   18.71  fun inferred_type (binding, _, mx) ctxt =
   18.72    let
   18.73      val x = Variable.name binding;
   18.74 -    val (T, ctxt') = ProofContext.inferred_param x ctxt
   18.75 +    val (T, ctxt') = Proof_Context.inferred_param x ctxt
   18.76    in ((x, T, mx), ctxt') end;
   18.77  
   18.78  fun polymorphic ctxt vars =
   18.79 @@ -280,7 +280,7 @@
   18.80        let
   18.81          val ((parms, rule), ctxt') =
   18.82            unify_params vars thesis_var raw_rule (Proof.context_of state');
   18.83 -        val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt';
   18.84 +        val (bind, _) = Proof_Context.bind_fixes (map (#1 o #1) parms) ctxt';
   18.85          val ts = map (bind o Free o #1) parms;
   18.86          val ps = map dest_Free ts;
   18.87          val asms =
   18.88 @@ -316,8 +316,8 @@
   18.89  
   18.90  in
   18.91  
   18.92 -val guess = gen_guess ProofContext.cert_vars;
   18.93 -val guess_cmd = gen_guess ProofContext.read_vars;
   18.94 +val guess = gen_guess Proof_Context.cert_vars;
   18.95 +val guess_cmd = gen_guess Proof_Context.read_vars;
   18.96  
   18.97  end;
   18.98  
    19.1 --- a/src/Pure/Isar/overloading.ML	Sat Apr 16 15:25:25 2011 +0200
    19.2 +++ b/src/Pure/Isar/overloading.ML	Sat Apr 16 15:47:52 2011 +0200
    19.3 @@ -65,8 +65,8 @@
    19.4    let
    19.5      val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
    19.6        ImprovableSyntax.get ctxt;
    19.7 -    val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
    19.8 -    val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt;
    19.9 +    val tsig = (Sign.tsig_of o Proof_Context.theory_of) ctxt;
   19.10 +    val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
   19.11      val passed_or_abbrev = passed orelse is_abbrev;
   19.12      fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
   19.13           of SOME ty_ty' => Type.typ_match tsig ty_ty'
   19.14 @@ -85,7 +85,7 @@
   19.15      if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
   19.16      if passed_or_abbrev then SOME (ts'', ctxt)
   19.17      else SOME (ts'', ctxt
   19.18 -      |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
   19.19 +      |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
   19.20        |> mark_passed)
   19.21    end;
   19.22  
   19.23 @@ -96,7 +96,7 @@
   19.24  
   19.25  fun improve_term_uncheck ts ctxt =
   19.26    let
   19.27 -    val thy = ProofContext.theory_of ctxt;
   19.28 +    val thy = Proof_Context.theory_of ctxt;
   19.29      val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
   19.30      val ts' = map (rewrite_liberal thy unchecks) ts;
   19.31    in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
   19.32 @@ -104,7 +104,7 @@
   19.33  fun set_primary_constraints ctxt =
   19.34    let
   19.35      val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
   19.36 -  in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
   19.37 +  in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
   19.38  
   19.39  val activate_improvable_syntax =
   19.40    Context.proof_map
   19.41 @@ -161,7 +161,7 @@
   19.42      val overloading = get_overloading lthy;
   19.43      fun pr_operation ((c, ty), (v, _)) =
   19.44        Pretty.block (Pretty.breaks
   19.45 -        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
   19.46 +        [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
   19.47            Pretty.str "::", Syntax.pretty_typ lthy ty]);
   19.48    in Pretty.str "overloading" :: map pr_operation overloading end;
   19.49  
   19.50 @@ -177,14 +177,14 @@
   19.51  
   19.52  fun gen_overloading prep_const raw_overloading thy =
   19.53    let
   19.54 -    val ctxt = ProofContext.init_global thy;
   19.55 +    val ctxt = Proof_Context.init_global thy;
   19.56      val _ = if null raw_overloading then error "At least one parameter must be given" else ();
   19.57      val overloading = raw_overloading |> map (fn (v, const, checked) =>
   19.58        (Term.dest_Const (prep_const ctxt const), (v, checked)));
   19.59    in
   19.60      thy
   19.61      |> Theory.checkpoint
   19.62 -    |> ProofContext.init_global
   19.63 +    |> Proof_Context.init_global
   19.64      |> Data.put overloading
   19.65      |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
   19.66      |> activate_improvable_syntax
    20.1 --- a/src/Pure/Isar/proof.ML	Sat Apr 16 15:25:25 2011 +0200
    20.2 +++ b/src/Pure/Isar/proof.ML	Sat Apr 16 15:47:52 2011 +0200
    20.3 @@ -166,8 +166,8 @@
    20.4    make_node (f (context, facts, mode, goal));
    20.5  
    20.6  val init_context =
    20.7 -  ProofContext.set_stmt true #>
    20.8 -  ProofContext.map_naming (K ProofContext.local_naming);
    20.9 +  Proof_Context.set_stmt true #>
   20.10 +  Proof_Context.map_naming (K Proof_Context.local_naming);
   20.11  
   20.12  fun init ctxt =
   20.13    State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
   20.14 @@ -200,7 +200,7 @@
   20.15  (* context *)
   20.16  
   20.17  val context_of = #context o current;
   20.18 -val theory_of = ProofContext.theory_of o context_of;
   20.19 +val theory_of = Proof_Context.theory_of o context_of;
   20.20  
   20.21  fun map_context f =
   20.22    map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   20.23 @@ -213,8 +213,8 @@
   20.24  fun propagate_ml_env state = map_contexts
   20.25    (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
   20.26  
   20.27 -val bind_terms = map_context o ProofContext.bind_terms;
   20.28 -val put_thms = map_context oo ProofContext.put_thms;
   20.29 +val bind_terms = map_context o Proof_Context.bind_terms;
   20.30 +val put_thms = map_context oo Proof_Context.put_thms;
   20.31  
   20.32  
   20.33  (* facts *)
   20.34 @@ -241,7 +241,7 @@
   20.35      NONE => put_facts NONE outer
   20.36    | SOME thms =>
   20.37        thms
   20.38 -      |> ProofContext.export (context_of inner) (context_of outer)
   20.39 +      |> Proof_Context.export (context_of inner) (context_of outer)
   20.40        |> (fn ths => put_facts (SOME ths) outer));
   20.41  
   20.42  
   20.43 @@ -324,7 +324,7 @@
   20.44  
   20.45  (** pretty_state **)
   20.46  
   20.47 -val verbose = ProofContext.verbose;
   20.48 +val verbose = Proof_Context.verbose;
   20.49  
   20.50  fun pretty_facts _ _ NONE = []
   20.51    | pretty_facts s ctxt (SOME ths) =
   20.52 @@ -357,8 +357,8 @@
   20.53        | prt_goal NONE = [];
   20.54  
   20.55      val prt_ctxt =
   20.56 -      if ! verbose orelse mode = Forward then ProofContext.pretty_context ctxt
   20.57 -      else if mode = Backward then ProofContext.pretty_ctxt ctxt
   20.58 +      if ! verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
   20.59 +      else if mode = Backward then Proof_Context.pretty_ctxt ctxt
   20.60        else [];
   20.61    in
   20.62      [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
   20.63 @@ -404,8 +404,8 @@
   20.64      Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
   20.65        state
   20.66        |> map_goal
   20.67 -          (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
   20.68 -           ProofContext.add_cases true meth_cases)
   20.69 +          (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #>
   20.70 +           Proof_Context.add_cases true meth_cases)
   20.71            (K (statement, [], using, goal', before_qed, after_qed)))
   20.72    end;
   20.73  
   20.74 @@ -465,7 +465,7 @@
   20.75      fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
   20.76    in
   20.77      raw_rules
   20.78 -    |> ProofContext.goal_export inner outer
   20.79 +    |> Proof_Context.goal_export inner outer
   20.80      |> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
   20.81    end;
   20.82  
   20.83 @@ -474,7 +474,7 @@
   20.84  
   20.85  fun conclude_goal ctxt goal propss =
   20.86    let
   20.87 -    val thy = ProofContext.theory_of ctxt;
   20.88 +    val thy = Proof_Context.theory_of ctxt;
   20.89      val string_of_term = Syntax.string_of_term ctxt;
   20.90      val string_of_thm = Display.string_of_thm ctxt;
   20.91  
   20.92 @@ -545,8 +545,8 @@
   20.93  
   20.94  in
   20.95  
   20.96 -val let_bind = gen_bind ProofContext.match_bind_i;
   20.97 -val let_bind_cmd = gen_bind ProofContext.match_bind;
   20.98 +val let_bind = gen_bind Proof_Context.match_bind_i;
   20.99 +val let_bind_cmd = gen_bind Proof_Context.match_bind;
  20.100  
  20.101  end;
  20.102  
  20.103 @@ -557,7 +557,7 @@
  20.104  
  20.105  fun gen_write prep_arg mode args =
  20.106    assert_forward
  20.107 -  #> map_context (fn ctxt => ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args))
  20.108 +  #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
  20.109    #> put_facts NONE;
  20.110  
  20.111  in
  20.112 @@ -566,7 +566,7 @@
  20.113  
  20.114  val write_cmd =
  20.115    gen_write (fn ctxt => fn (c, mx) =>
  20.116 -    (ProofContext.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
  20.117 +    (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
  20.118  
  20.119  end;
  20.120  
  20.121 @@ -577,13 +577,13 @@
  20.122  
  20.123  fun gen_fix prep_vars args =
  20.124    assert_forward
  20.125 -  #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
  20.126 +  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (prep_vars ctxt args) ctxt))
  20.127    #> put_facts NONE;
  20.128  
  20.129  in
  20.130  
  20.131  val fix = gen_fix (K I);
  20.132 -val fix_cmd = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
  20.133 +val fix_cmd = gen_fix (fn ctxt => fn args => fst (Proof_Context.read_vars args ctxt));
  20.134  
  20.135  end;
  20.136  
  20.137 @@ -600,8 +600,8 @@
  20.138  
  20.139  in
  20.140  
  20.141 -val assm = gen_assume ProofContext.add_assms_i (K I);
  20.142 -val assm_cmd = gen_assume ProofContext.add_assms Attrib.attribute;
  20.143 +val assm = gen_assume Proof_Context.add_assms_i (K I);
  20.144 +val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute;
  20.145  val assume = assm Assumption.assume_export;
  20.146  val assume_cmd = assm_cmd Assumption.assume_export;
  20.147  val presume = assm Assumption.presume_export;
  20.148 @@ -633,8 +633,8 @@
  20.149  
  20.150  in
  20.151  
  20.152 -val def = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
  20.153 -val def_cmd = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
  20.154 +val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
  20.155 +val def_cmd = gen_def Attrib.attribute Proof_Context.read_vars Proof_Context.match_bind;
  20.156  
  20.157  end;
  20.158  
  20.159 @@ -666,7 +666,7 @@
  20.160  fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
  20.161    state
  20.162    |> assert_forward
  20.163 -  |> map_context_result (ProofContext.note_thmss ""
  20.164 +  |> map_context_result (Proof_Context.note_thmss ""
  20.165      (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
  20.166    |> these_factss (more_facts state)
  20.167    ||> opt_chain
  20.168 @@ -675,13 +675,13 @@
  20.169  in
  20.170  
  20.171  val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
  20.172 -val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
  20.173 +val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute Proof_Context.get_fact;
  20.174  
  20.175  val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
  20.176 -val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
  20.177 +val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
  20.178  
  20.179  val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
  20.180 -val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
  20.181 +val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
  20.182  
  20.183  val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
  20.184  
  20.185 @@ -696,7 +696,7 @@
  20.186    state
  20.187    |> assert_backward
  20.188    |> map_context_result
  20.189 -    (ProofContext.note_thmss ""
  20.190 +    (Proof_Context.note_thmss ""
  20.191        (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
  20.192          (no_binding args)))
  20.193    |> (fn (named_facts, state') =>
  20.194 @@ -713,9 +713,9 @@
  20.195  in
  20.196  
  20.197  val using = gen_using append_using (K (K I)) (K I) (K I);
  20.198 -val using_cmd = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
  20.199 +val using_cmd = gen_using append_using (K (K I)) Attrib.attribute Proof_Context.get_fact;
  20.200  val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
  20.201 -val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
  20.202 +val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute Proof_Context.get_fact;
  20.203  
  20.204  end;
  20.205  
  20.206 @@ -731,7 +731,7 @@
  20.207    let
  20.208      val atts = map (prep_att (theory_of state)) raw_atts;
  20.209      val (asms, state') = state |> map_context_result (fn ctxt =>
  20.210 -      ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
  20.211 +      ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
  20.212      val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
  20.213    in
  20.214      state'
  20.215 @@ -881,7 +881,7 @@
  20.216      goal_state
  20.217      |> map_context (init_context #> Variable.set_body true)
  20.218      |> put_goal (SOME (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')))
  20.219 -    |> map_context (ProofContext.auto_bind_goal props)
  20.220 +    |> map_context (Proof_Context.auto_bind_goal props)
  20.221      |> chaining ? (`the_facts #-> using_facts)
  20.222      |> put_facts NONE
  20.223      |> open_block
  20.224 @@ -902,7 +902,7 @@
  20.225        |> Variable.exportT_terms goal_ctxt outer_ctxt;
  20.226      val results =
  20.227        tl (conclude_goal goal_ctxt goal stmt)
  20.228 -      |> burrow (ProofContext.export goal_ctxt outer_ctxt);
  20.229 +      |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
  20.230    in
  20.231      outer_state
  20.232      |> map_context (after_ctxt props)
  20.233 @@ -932,7 +932,7 @@
  20.234  
  20.235  fun local_qeds txt =
  20.236    end_proof false txt
  20.237 -  #> Seq.map (generic_qed ProofContext.auto_bind_facts #->
  20.238 +  #> Seq.map (generic_qed Proof_Context.auto_bind_facts #->
  20.239      (fn ((after_qed, _), results) => after_qed results));
  20.240  
  20.241  fun local_qed txt = local_qeds txt #> check_finish;
  20.242 @@ -942,10 +942,10 @@
  20.243  
  20.244  fun global_goal prepp before_qed after_qed propp ctxt =
  20.245    init ctxt
  20.246 -  |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
  20.247 +  |> generic_goal (prepp #> Proof_Context.auto_fixes) "" before_qed (K I, after_qed) propp;
  20.248  
  20.249 -val theorem = global_goal ProofContext.bind_propp_schematic_i;
  20.250 -val theorem_cmd = global_goal ProofContext.bind_propp_schematic;
  20.251 +val theorem = global_goal Proof_Context.bind_propp_schematic_i;
  20.252 +val theorem_cmd = global_goal Proof_Context.bind_propp_schematic;
  20.253  
  20.254  fun global_qeds txt =
  20.255    end_proof true txt
  20.256 @@ -1017,10 +1017,10 @@
  20.257  
  20.258  in
  20.259  
  20.260 -val have = gen_have (K I) ProofContext.bind_propp_i;
  20.261 -val have_cmd = gen_have Attrib.attribute ProofContext.bind_propp;
  20.262 -val show = gen_show (K I) ProofContext.bind_propp_i;
  20.263 -val show_cmd = gen_show Attrib.attribute ProofContext.bind_propp;
  20.264 +val have = gen_have (K I) Proof_Context.bind_propp_i;
  20.265 +val have_cmd = gen_have Attrib.attribute Proof_Context.bind_propp;
  20.266 +val show = gen_show (K I) Proof_Context.bind_propp_i;
  20.267 +val show_cmd = gen_show Attrib.attribute Proof_Context.bind_propp;
  20.268  
  20.269  end;
  20.270  
  20.271 @@ -1064,9 +1064,9 @@
  20.272        (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
  20.273  
  20.274      fun after_local' [[th]] = put_thms false (Auto_Bind.thisN, SOME [th]);
  20.275 -    fun after_global' [[th]] = ProofContext.put_thms false (Auto_Bind.thisN, SOME [th]);
  20.276 +    fun after_global' [[th]] = Proof_Context.put_thms false (Auto_Bind.thisN, SOME [th]);
  20.277      val after_qed' = (after_local', after_global');
  20.278 -    val this_name = ProofContext.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
  20.279 +    val this_name = Proof_Context.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
  20.280  
  20.281      val result_ctxt =
  20.282        state
  20.283 @@ -1075,7 +1075,7 @@
  20.284        |> fork_proof;
  20.285  
  20.286      val future_thm = result_ctxt |> Future.map (fn (_, x) =>
  20.287 -      ProofContext.get_fact_single (get_context x) (Facts.named this_name));
  20.288 +      Proof_Context.get_fact_single (get_context x) (Facts.named this_name));
  20.289      val finished_goal = Goal.future_result goal_ctxt future_thm prop';
  20.290      val state' =
  20.291        state
    21.1 --- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 15:25:25 2011 +0200
    21.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 15:47:52 2011 +0200
    21.3 @@ -161,10 +161,10 @@
    21.4    val pretty_context: Proof.context -> Pretty.T list
    21.5  end;
    21.6  
    21.7 -structure ProofContext: PROOF_CONTEXT =
    21.8 +structure Proof_Context: PROOF_CONTEXT =
    21.9  struct
   21.10  
   21.11 -open ProofContext;
   21.12 +open Proof_Context;
   21.13  
   21.14  
   21.15  (** inner syntax mode **)
   21.16 @@ -597,7 +597,7 @@
   21.17  
   21.18  local
   21.19  
   21.20 -val dummies = Config.bool (Config.declare "ProofContext.dummies" (K (Config.Bool false)));
   21.21 +val dummies = Config.bool (Config.declare "Proof_Context.dummies" (K (Config.Bool false)));
   21.22  
   21.23  fun check_dummies ctxt t =
   21.24    if Config.get ctxt dummies then t
   21.25 @@ -1345,5 +1345,5 @@
   21.26  
   21.27  end;
   21.28  
   21.29 -val show_abbrevs = ProofContext.show_abbrevs;
   21.30 +val show_abbrevs = Proof_Context.show_abbrevs;
   21.31  
    22.1 --- a/src/Pure/Isar/proof_display.ML	Sat Apr 16 15:25:25 2011 +0200
    22.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Apr 16 15:47:52 2011 +0200
    22.3 @@ -27,8 +27,8 @@
    22.4  (* toplevel pretty printing *)
    22.5  
    22.6  fun pp_context ctxt =
    22.7 - (if ! ProofContext.debug then
    22.8 -    Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    22.9 + (if ! Proof_Context.debug then
   22.10 +    Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   22.11    else Pretty.str "<context>");
   22.12  
   22.13  fun pp_thm th =
   22.14 @@ -48,7 +48,7 @@
   22.15  
   22.16  fun pretty_theorems_diff verbose prev_thys thy =
   22.17    let
   22.18 -    val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
   22.19 +    val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
   22.20      val facts = Global_Theory.facts_of thy;
   22.21      val thmss =
   22.22        Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
   22.23 @@ -87,7 +87,7 @@
   22.24  
   22.25  fun pretty_facts ctxt =
   22.26    flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
   22.27 -    map (single o ProofContext.pretty_fact_aux ctxt false);
   22.28 +    map (single o Proof_Context.pretty_fact_aux ctxt false);
   22.29  
   22.30  in
   22.31  
   22.32 @@ -98,7 +98,7 @@
   22.33    else Pretty.writeln
   22.34      (case facts of
   22.35        [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   22.36 -        ProofContext.pretty_fact_aux ctxt false fact])
   22.37 +        Proof_Context.pretty_fact_aux ctxt false fact])
   22.38      | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   22.39          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
   22.40  
   22.41 @@ -118,7 +118,7 @@
   22.42  in
   22.43  
   22.44  fun pretty_consts ctxt pred cs =
   22.45 -  (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
   22.46 +  (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
   22.47      [] => pretty_vars ctxt "constants" cs
   22.48    | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
   22.49  
    23.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Apr 16 15:25:25 2011 +0200
    23.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Apr 16 15:47:52 2011 +0200
    23.3 @@ -83,7 +83,7 @@
    23.4      val ts = map2 parse Ts ss;
    23.5      val ts' =
    23.6        map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
    23.7 -      |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
    23.8 +      |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
    23.9        |> Variable.polymorphic ctxt;
   23.10      val Ts' = map Term.fastype_of ts';
   23.11      val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
   23.12 @@ -91,7 +91,7 @@
   23.13  
   23.14  fun read_insts ctxt mixed_insts (tvars, vars) =
   23.15    let
   23.16 -    val thy = ProofContext.theory_of ctxt;
   23.17 +    val thy = Proof_Context.theory_of ctxt;
   23.18      val cert = Thm.cterm_of thy;
   23.19      val certT = Thm.ctyp_of thy;
   23.20  
   23.21 @@ -193,7 +193,7 @@
   23.22  (* instantiation of rule or goal state *)
   23.23  
   23.24  fun read_instantiate ctxt args thm =
   23.25 -  read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
   23.26 +  read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic)  (* FIXME !? *)
   23.27      (map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
   23.28  
   23.29  fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
   23.30 @@ -260,7 +260,7 @@
   23.31  
   23.32  fun bires_inst_tac bires_flag ctxt insts thm =
   23.33    let
   23.34 -    val thy = ProofContext.theory_of ctxt;
   23.35 +    val thy = Proof_Context.theory_of ctxt;
   23.36      (* Separate type and term insts *)
   23.37      fun has_type_var ((x, _), _) =
   23.38        (case Symbol.explode x of "'" :: _ => true | _ => false);
   23.39 @@ -279,7 +279,7 @@
   23.40          val (param_names, ctxt') = ctxt
   23.41            |> Variable.declare_thm thm
   23.42            |> Thm.fold_terms Variable.declare_constraints st
   23.43 -          |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
   23.44 +          |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
   23.45  
   23.46          (* Process type insts: Tinsts_env *)
   23.47          fun absent xi = error
    24.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Apr 16 15:25:25 2011 +0200
    24.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Apr 16 15:47:52 2011 +0200
    24.3 @@ -35,10 +35,10 @@
    24.4    (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
    24.5      (fn args => fn st =>
    24.6        if ! quick_and_dirty
    24.7 -      then cheat_tac (ProofContext.theory_of ctxt) st
    24.8 +      then cheat_tac (Proof_Context.theory_of ctxt) st
    24.9        else tac args st);
   24.10  
   24.11  fun prove_global thy xs asms prop tac =
   24.12 -  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
   24.13 +  Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
   24.14  
   24.15  end;
    25.1 --- a/src/Pure/Isar/spec_rules.ML	Sat Apr 16 15:25:25 2011 +0200
    25.2 +++ b/src/Pure/Isar/spec_rules.ML	Sat Apr 16 15:47:52 2011 +0200
    25.3 @@ -48,7 +48,7 @@
    25.4  
    25.5  fun add class (ts, ths) lthy =
    25.6    let
    25.7 -    val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts;
    25.8 +    val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
    25.9    in
   25.10      lthy |> Local_Theory.declaration true
   25.11        (fn phi =>
    26.1 --- a/src/Pure/Isar/specification.ML	Sat Apr 16 15:25:25 2011 +0200
    26.2 +++ b/src/Pure/Isar/specification.ML	Sat Apr 16 15:47:52 2011 +0200
    26.3 @@ -117,10 +117,10 @@
    26.4  
    26.5  fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
    26.6    let
    26.7 -    val thy = ProofContext.theory_of ctxt;
    26.8 +    val thy = Proof_Context.theory_of ctxt;
    26.9  
   26.10      val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
   26.11 -    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
   26.12 +    val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
   26.13  
   26.14      val Asss =
   26.15        (map o map) snd raw_specss
   26.16 @@ -137,7 +137,7 @@
   26.17        |> flat |> burrow (Syntax.check_props params_ctxt);
   26.18      val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
   26.19  
   26.20 -    val Ts = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
   26.21 +    val Ts = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
   26.22      val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
   26.23      val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
   26.24    in ((params, name_atts ~~ specs), specs_ctxt) end;
   26.25 @@ -152,17 +152,17 @@
   26.26  
   26.27  in
   26.28  
   26.29 -fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;
   26.30 -fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true x;
   26.31 +fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x;
   26.32 +fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true x;
   26.33  
   26.34 -fun check_free_spec x = prep_spec ProofContext.cert_vars (K I) (K I) false x;
   26.35 -fun read_free_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src false x;
   26.36 +fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x;
   26.37 +fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src false x;
   26.38  
   26.39  fun check_specification vars specs =
   26.40 -  prepare ProofContext.cert_vars (K I) (K I) true vars [specs];
   26.41 +  prepare Proof_Context.cert_vars (K I) (K I) true vars [specs];
   26.42  
   26.43  fun read_specification vars specs =
   26.44 -  prepare ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
   26.45 +  prepare Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
   26.46  
   26.47  end;
   26.48  
   26.49 @@ -171,7 +171,7 @@
   26.50  
   26.51  fun gen_axioms do_print prep raw_vars raw_specs thy =
   26.52    let
   26.53 -    val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init_global thy);
   26.54 +    val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
   26.55      val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars;
   26.56  
   26.57      (*consts*)
   26.58 @@ -246,7 +246,7 @@
   26.59    let
   26.60      val ((vars, [(_, prop)]), _) =
   26.61        prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
   26.62 -        (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
   26.63 +        (lthy |> Proof_Context.set_mode Proof_Context.mode_abbrev);
   26.64      val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
   26.65      val var =
   26.66        (case vars of
   26.67 @@ -259,9 +259,9 @@
   26.68                  Position.str_of (Binding.pos_of b));
   26.69            in (b, mx) end);
   26.70      val lthy' = lthy
   26.71 -      |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
   26.72 +      |> Proof_Context.set_syntax_mode mode    (* FIXME ?!? *)
   26.73        |> Local_Theory.abbrev mode (var, rhs) |> snd
   26.74 -      |> ProofContext.restore_syntax_mode lthy;
   26.75 +      |> Proof_Context.restore_syntax_mode lthy;
   26.76  
   26.77      val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
   26.78    in lthy' end;
   26.79 @@ -283,10 +283,10 @@
   26.80  in
   26.81  
   26.82  val type_notation = gen_type_notation (K I);
   26.83 -val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
   26.84 +val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false);
   26.85  
   26.86  val notation = gen_notation (K I);
   26.87 -val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false dummyT);
   26.88 +val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);
   26.89  
   26.90  end;
   26.91  
   26.92 @@ -295,7 +295,7 @@
   26.93  
   26.94  fun gen_theorems prep_fact prep_att kind raw_facts lthy =
   26.95    let
   26.96 -    val attrib = prep_att (ProofContext.theory_of lthy);
   26.97 +    val attrib = prep_att (Proof_Context.theory_of lthy);
   26.98      val facts = raw_facts |> map (fn ((name, atts), bs) =>
   26.99        ((name, map attrib atts),
  26.100          bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
  26.101 @@ -304,7 +304,7 @@
  26.102    in (res, lthy') end;
  26.103  
  26.104  val theorems = gen_theorems (K I) (K I);
  26.105 -val theorems_cmd = gen_theorems ProofContext.get_fact Attrib.intern_src;
  26.106 +val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src;
  26.107  
  26.108  
  26.109  (* complex goal statements *)
  26.110 @@ -331,7 +331,7 @@
  26.111          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
  26.112          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
  26.113  
  26.114 -        val thesis = Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
  26.115 +        val thesis = Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) Auto_Bind.thesisN;
  26.116  
  26.117          fun assume_case ((name, (vars, _)), asms) ctxt' =
  26.118            let
  26.119 @@ -340,12 +340,12 @@
  26.120              val props = map fst asms;
  26.121              val (Ts, _) = ctxt'
  26.122                |> fold Variable.declare_term props
  26.123 -              |> fold_map ProofContext.inferred_param xs;
  26.124 +              |> fold_map Proof_Context.inferred_param xs;
  26.125              val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
  26.126            in
  26.127 -            ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
  26.128 +            ctxt' |> (snd o Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
  26.129              ctxt' |> Variable.auto_fixes asm
  26.130 -            |> ProofContext.add_assms_i Assumption.assume_export
  26.131 +            |> Proof_Context.add_assms_i Assumption.assume_export
  26.132                [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
  26.133              |>> (fn [(_, [th])] => th)
  26.134            end;
  26.135 @@ -356,10 +356,10 @@
  26.136          val stmt = [((Binding.empty, atts), [(thesis, [])])];
  26.137  
  26.138          val (facts, goal_ctxt) = elems_ctxt
  26.139 -          |> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
  26.140 +          |> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
  26.141            |> fold_map assume_case (obtains ~~ propp)
  26.142            |-> (fn ths =>
  26.143 -            ProofContext.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
  26.144 +            Proof_Context.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
  26.145              #2 #> pair ths);
  26.146        in ((prems, stmt, SOME facts), goal_ctxt) end);
  26.147  
  26.148 @@ -375,7 +375,7 @@
  26.149      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
  26.150    let
  26.151      val _ = Local_Theory.affirm lthy;
  26.152 -    val thy = ProofContext.theory_of lthy;
  26.153 +    val thy = Proof_Context.theory_of lthy;
  26.154  
  26.155      val attrib = prep_att thy;
  26.156      val atts = map attrib raw_atts;
  26.157 @@ -385,7 +385,7 @@
  26.158  
  26.159      fun after_qed' results goal_ctxt' =
  26.160        let val results' =
  26.161 -        burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
  26.162 +        burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results
  26.163        in
  26.164          lthy
  26.165          |> Local_Theory.notes_kind kind
  26.166 @@ -403,7 +403,7 @@
  26.167        end;
  26.168    in
  26.169      goal_ctxt
  26.170 -    |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
  26.171 +    |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
  26.172      |> snd
  26.173      |> Proof.theorem before_qed after_qed' (map snd stmt)
  26.174      |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
    27.1 --- a/src/Pure/Isar/toplevel.ML	Sat Apr 16 15:25:25 2011 +0200
    27.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Apr 16 15:47:52 2011 +0200
    27.3 @@ -516,7 +516,7 @@
    27.4  
    27.5  fun theory_to_proof f = begin_proof
    27.6    (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
    27.7 -  (K (Context.Theory o Sign.reset_group o ProofContext.theory_of));
    27.8 +  (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
    27.9  
   27.10  end;
   27.11  
   27.12 @@ -660,7 +660,7 @@
   27.13      else
   27.14        let
   27.15          val (body_trs, end_tr) = split_last proof_trs;
   27.16 -        val finish = Context.Theory o ProofContext.theory_of;
   27.17 +        val finish = Context.Theory o Proof_Context.theory_of;
   27.18  
   27.19          val future_proof = Proof.global_future_proof
   27.20            (fn prf =>
    28.1 --- a/src/Pure/Isar/typedecl.ML	Sat Apr 16 15:25:25 2011 +0200
    28.2 +++ b/src/Pure/Isar/typedecl.ML	Sat Apr 16 15:47:52 2011 +0200
    28.3 @@ -51,7 +51,7 @@
    28.4      fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
    28.5  
    28.6      val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
    28.7 -    val args = map (TFree o ProofContext.check_tfree lthy) raw_args;
    28.8 +    val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
    28.9      val T = Type (Local_Theory.full_name lthy b, args);
   28.10  
   28.11      val bad_args =
   28.12 @@ -98,7 +98,7 @@
   28.13  
   28.14  fun read_abbrev b ctxt raw_rhs =
   28.15    let
   28.16 -    val rhs = ProofContext.read_typ_syntax (ctxt |> ProofContext.set_defsort []) raw_rhs;
   28.17 +    val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs;
   28.18      val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
   28.19      val _ =
   28.20        if null ignored then ()
   28.21 @@ -110,7 +110,7 @@
   28.22  
   28.23  in
   28.24  
   28.25 -val abbrev = gen_abbrev (K ProofContext.cert_typ_syntax);
   28.26 +val abbrev = gen_abbrev (K Proof_Context.cert_typ_syntax);
   28.27  val abbrev_cmd = gen_abbrev read_abbrev;
   28.28  
   28.29  end;
    29.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Apr 16 15:25:25 2011 +0200
    29.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sat Apr 16 15:47:52 2011 +0200
    29.3 @@ -80,12 +80,12 @@
    29.4  val _ = macro "let" (Args.context --
    29.5    Scan.lift
    29.6      (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
    29.7 -    >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
    29.8 +    >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt)));
    29.9  
   29.10  val _ = macro "note" (Args.context :|-- (fn ctxt =>
   29.11    Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
   29.12 -    ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
   29.13 -  >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
   29.14 +    ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
   29.15 +  >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt))));
   29.16  
   29.17  val _ = value "ctyp" (Args.typ >> (fn T =>
   29.18    "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
   29.19 @@ -97,14 +97,14 @@
   29.20    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
   29.21  
   29.22  val _ = value "cpat"
   29.23 -  (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
   29.24 +  (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   29.25      "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
   29.26  
   29.27  
   29.28  (* type classes *)
   29.29  
   29.30  fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
   29.31 -  ProofContext.read_class ctxt s
   29.32 +  Proof_Context.read_class ctxt s
   29.33    |> syn ? Lexicon.mark_class
   29.34    |> ML_Syntax.print_string);
   29.35  
   29.36 @@ -120,8 +120,8 @@
   29.37  fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
   29.38    >> (fn (ctxt, (s, pos)) =>
   29.39      let
   29.40 -      val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
   29.41 -      val decl = Type.the_decl (ProofContext.tsig_of ctxt) c;
   29.42 +      val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
   29.43 +      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) c;
   29.44        val res =
   29.45          (case try check (c, decl) of
   29.46            SOME res => res
   29.47 @@ -139,8 +139,8 @@
   29.48  fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
   29.49    >> (fn (ctxt, (s, pos)) =>
   29.50      let
   29.51 -      val Const (c, _) = ProofContext.read_const_proper ctxt false s;
   29.52 -      val res = check (ProofContext.consts_of ctxt, c)
   29.53 +      val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
   29.54 +      val res = check (Proof_Context.consts_of ctxt, c)
   29.55          handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
   29.56      in ML_Syntax.print_string res end);
   29.57  
   29.58 @@ -151,7 +151,7 @@
   29.59  
   29.60  val _ = inline "syntax_const"
   29.61    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   29.62 -    if is_some (Syntax.lookup_const (ProofContext.syn_of ctxt) c)
   29.63 +    if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   29.64      then ML_Syntax.print_string c
   29.65      else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
   29.66  
   29.67 @@ -160,8 +160,8 @@
   29.68        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   29.69      >> (fn ((ctxt, raw_c), Ts) =>
   29.70        let
   29.71 -        val Const (c, _) = ProofContext.read_const_proper ctxt true raw_c;
   29.72 -        val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts));
   29.73 +        val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
   29.74 +        val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
   29.75        in ML_Syntax.atomic (ML_Syntax.print_term const) end));
   29.76  
   29.77  end;
    30.1 --- a/src/Pure/ML/ml_context.ML	Sat Apr 16 15:25:25 2011 +0200
    30.2 +++ b/src/Pure/ML/ml_context.ML	Sat Apr 16 15:47:52 2011 +0200
    30.3 @@ -48,8 +48,8 @@
    30.4  val the_global_context = Context.theory_of o the_generic_context;
    30.5  val the_local_context = Context.proof_of o the_generic_context;
    30.6  
    30.7 -fun thm name = ProofContext.get_thm (the_local_context ()) name;
    30.8 -fun thms name = ProofContext.get_thms (the_local_context ()) name;
    30.9 +fun thm name = Proof_Context.get_thm (the_local_context ()) name;
   30.10 +fun thms name = Proof_Context.get_thms (the_local_context ()) name;
   30.11  
   30.12  fun exec (e: unit -> unit) context =
   30.13    (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
    31.1 --- a/src/Pure/ML/ml_thms.ML	Sat Apr 16 15:25:25 2011 +0200
    31.2 +++ b/src/Pure/ML/ml_thms.ML	Sat Apr 16 15:47:52 2011 +0200
    31.3 @@ -62,7 +62,7 @@
    31.4          val i = serial ();
    31.5          val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
    31.6          fun after_qed res goal_ctxt =
    31.7 -          put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
    31.8 +          put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
    31.9          val ctxt' = ctxt
   31.10            |> Proof.theorem NONE after_qed propss
   31.11            |> Proof.global_terminal_proof methods;
    32.1 --- a/src/Pure/Proof/extraction.ML	Sat Apr 16 15:25:25 2011 +0200
    32.2 +++ b/src/Pure/Proof/extraction.ML	Sat Apr 16 15:47:52 2011 +0200
    32.3 @@ -162,9 +162,9 @@
    32.4  
    32.5  fun read_term thy T s =
    32.6    let
    32.7 -    val ctxt = ProofContext.init_global thy
    32.8 +    val ctxt = Proof_Context.init_global thy
    32.9        |> Proof_Syntax.strip_sorts_consttypes
   32.10 -      |> ProofContext.set_defsort [];
   32.11 +      |> Proof_Context.set_defsort [];
   32.12      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   32.13    in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
   32.14  
    33.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Apr 16 15:25:25 2011 +0200
    33.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Apr 16 15:47:52 2011 +0200
    33.3 @@ -202,9 +202,9 @@
    33.4    end;
    33.5  
    33.6  fun strip_sorts_consttypes ctxt =
    33.7 -  let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt)
    33.8 +  let val {constants = (_, tab), ...} = Consts.dest (Proof_Context.consts_of ctxt)
    33.9    in Symtab.fold (fn (s, (T, _)) =>
   33.10 -      ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T)))
   33.11 +      Proof_Context.add_const_constraint (s, SOME (Type.strip_sorts T)))
   33.12      tab ctxt
   33.13    end;
   33.14  
   33.15 @@ -216,12 +216,12 @@
   33.16        |> add_proof_syntax
   33.17        |> add_proof_atom_consts
   33.18          (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
   33.19 -      |> ProofContext.init_global
   33.20 -      |> ProofContext.allow_dummies
   33.21 -      |> ProofContext.set_mode ProofContext.mode_schematic
   33.22 +      |> Proof_Context.init_global
   33.23 +      |> Proof_Context.allow_dummies
   33.24 +      |> Proof_Context.set_mode Proof_Context.mode_schematic
   33.25        |> (if topsort then
   33.26              strip_sorts_consttypes #>
   33.27 -            ProofContext.set_defsort []
   33.28 +            Proof_Context.set_defsort []
   33.29            else I);
   33.30    in
   33.31      fn ty => fn s =>
   33.32 @@ -259,8 +259,8 @@
   33.33    in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
   33.34  
   33.35  fun pretty_proof ctxt prf =
   33.36 -  ProofContext.pretty_term_abbrev
   33.37 -    (ProofContext.transfer_syntax (proof_syntax prf (ProofContext.theory_of ctxt)) ctxt)
   33.38 +  Proof_Context.pretty_term_abbrev
   33.39 +    (Proof_Context.transfer_syntax (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
   33.40      (term_of_proof prf);
   33.41  
   33.42  fun pretty_proof_of ctxt full th =
    34.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 16 15:25:25 2011 +0200
    34.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 16 15:47:52 2011 +0200
    34.3 @@ -522,7 +522,7 @@
    34.4  
    34.5  fun thms_of_thy name =
    34.6    let val thy = Thy_Info.get_theory name
    34.7 -  in map fst (theory_facts thy |-> Facts.extern_static (ProofContext.init_global thy)) end;
    34.8 +  in map fst (theory_facts thy |-> Facts.extern_static (Proof_Context.init_global thy)) end;
    34.9  
   34.10  fun qualified_thms_of_thy name =
   34.11    map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static);
   34.12 @@ -610,7 +610,7 @@
   34.13                  (* TODO: interim: this is probably not right.
   34.14                     What we want is mapping onto simple PGIP name/context model. *)
   34.15                  val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
   34.16 -                val thy = ProofContext.theory_of ctx
   34.17 +                val thy = Proof_Context.theory_of ctx
   34.18                  val ths = [Global_Theory.get_thm thy thmname]
   34.19                  val deps = #2 (thms_deps ths);
   34.20              in
    35.1 --- a/src/Pure/Syntax/syntax.ML	Sat Apr 16 15:25:25 2011 +0200
    35.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Apr 16 15:47:52 2011 +0200
    35.3 @@ -344,10 +344,10 @@
    35.4  val read_term = singleton o read_terms;
    35.5  val read_prop = singleton o read_props;
    35.6  
    35.7 -val read_sort_global = read_sort o ProofContext.init_global;
    35.8 -val read_typ_global = read_typ o ProofContext.init_global;
    35.9 -val read_term_global = read_term o ProofContext.init_global;
   35.10 -val read_prop_global = read_prop o ProofContext.init_global;
   35.11 +val read_sort_global = read_sort o Proof_Context.init_global;
   35.12 +val read_typ_global = read_typ o Proof_Context.init_global;
   35.13 +val read_term_global = read_term o Proof_Context.init_global;
   35.14 +val read_prop_global = read_prop o Proof_Context.init_global;
   35.15  
   35.16  
   35.17  (* pretty = uncheck + unparse *)
   35.18 @@ -370,7 +370,7 @@
   35.19  val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
   35.20  fun is_pretty_global ctxt = Config.get ctxt pretty_global;
   35.21  val set_pretty_global = Config.put pretty_global;
   35.22 -val init_pretty_global = set_pretty_global true o ProofContext.init_global;
   35.23 +val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
   35.24  
   35.25  val pretty_term_global = pretty_term o init_pretty_global;
   35.26  val pretty_typ_global = pretty_typ o init_pretty_global;
    36.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 15:25:25 2011 +0200
    36.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 15:47:52 2011 +0200
    36.3 @@ -21,13 +21,13 @@
    36.4  (** markup logical entities **)
    36.5  
    36.6  fun markup_class ctxt c =
    36.7 -  [Name_Space.markup_entry (Type.class_space (ProofContext.tsig_of ctxt)) c];
    36.8 +  [Name_Space.markup_entry (Type.class_space (Proof_Context.tsig_of ctxt)) c];
    36.9  
   36.10  fun markup_type ctxt c =
   36.11 -  [Name_Space.markup_entry (Type.type_space (ProofContext.tsig_of ctxt)) c];
   36.12 +  [Name_Space.markup_entry (Type.type_space (Proof_Context.tsig_of ctxt)) c];
   36.13  
   36.14  fun markup_const ctxt c =
   36.15 -  [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c];
   36.16 +  [Name_Space.markup_entry (Consts.space_of (Proof_Context.consts_of ctxt)) c];
   36.17  
   36.18  fun markup_free ctxt x =
   36.19    [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
   36.20 @@ -40,7 +40,7 @@
   36.21    [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
   36.22  
   36.23  fun markup_entity ctxt c =
   36.24 -  (case Syntax.lookup_const (ProofContext.syn_of ctxt) c of
   36.25 +  (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
   36.26      SOME "" => []
   36.27    | SOME b => markup_entity ctxt b
   36.28    | NONE => c |> Lexicon.unmark
   36.29 @@ -125,8 +125,8 @@
   36.30  
   36.31  fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   36.32    let
   36.33 -    val get_class = ProofContext.read_class ctxt;
   36.34 -    val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
   36.35 +    val get_class = Proof_Context.read_class ctxt;
   36.36 +    val get_type = #1 o dest_Type o Proof_Context.read_type_name_proper ctxt false;
   36.37  
   36.38      val reports = Unsynchronized.ref ([]: Position.reports);
   36.39      fun report pos = Position.reports reports [pos];
   36.40 @@ -197,11 +197,11 @@
   36.41    | decode_term ctxt (reports0, Exn.Result tm) =
   36.42        let
   36.43          fun get_const a =
   36.44 -          ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
   36.45 -            handle ERROR _ => (false, Consts.intern (ProofContext.consts_of ctxt) a));
   36.46 -        val get_free = ProofContext.intern_skolem ctxt;
   36.47 +          ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
   36.48 +            handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
   36.49 +        val get_free = Proof_Context.intern_skolem ctxt;
   36.50  
   36.51 -        val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
   36.52 +        val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
   36.53  
   36.54          val reports = Unsynchronized.ref reports0;
   36.55          fun report ps = Position.reports reports ps;
   36.56 @@ -272,7 +272,7 @@
   36.57  
   36.58  fun parse_asts ctxt raw root (syms, pos) =
   36.59    let
   36.60 -    val syn = ProofContext.syn_of ctxt;
   36.61 +    val syn = Proof_Context.syn_of ctxt;
   36.62      val ast_tr = Syntax.parse_ast_translation syn;
   36.63  
   36.64      val toks = Syntax.tokenize syn raw syms;
   36.65 @@ -301,7 +301,7 @@
   36.66  
   36.67  fun parse_raw ctxt root input =
   36.68    let
   36.69 -    val syn = ProofContext.syn_of ctxt;
   36.70 +    val syn = Proof_Context.syn_of ctxt;
   36.71      val tr = Syntax.parse_translation syn;
   36.72      val parse_rules = Syntax.parse_rules syn;
   36.73    in
   36.74 @@ -325,7 +325,7 @@
   36.75        |> report_result ctxt pos
   36.76        |> sort_of_term
   36.77        handle ERROR msg => parse_failed ctxt pos msg "sort";
   36.78 -  in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
   36.79 +  in Type.minimize_sort (Proof_Context.tsig_of ctxt) S end;
   36.80  
   36.81  fun parse_typ ctxt text =
   36.82    let
   36.83 @@ -333,7 +333,7 @@
   36.84      val T =
   36.85        parse_raw ctxt "type" (syms, pos)
   36.86        |> report_result ctxt pos
   36.87 -      |> (fn t => typ_of_term (ProofContext.get_sort ctxt (term_sorts t)) t)
   36.88 +      |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
   36.89        handle ERROR msg => parse_failed ctxt pos msg "type";
   36.90    in T end;
   36.91  
   36.92 @@ -398,7 +398,7 @@
   36.93  
   36.94  fun parse_ast_pattern ctxt (root, str) =
   36.95    let
   36.96 -    val syn = ProofContext.syn_of ctxt;
   36.97 +    val syn = Proof_Context.syn_of ctxt;
   36.98  
   36.99      fun constify (ast as Ast.Constant _) = ast
  36.100        | constify (ast as Ast.Variable x) =
  36.101 @@ -590,7 +590,7 @@
  36.102        else Markup.hilite;
  36.103    in
  36.104      if can Name.dest_skolem x
  36.105 -    then ([m, Markup.skolem], ProofContext.revert_skolem ctxt x)
  36.106 +    then ([m, Markup.skolem], Proof_Context.revert_skolem ctxt x)
  36.107      else ([m, Markup.free], x)
  36.108    end;
  36.109  
  36.110 @@ -604,7 +604,7 @@
  36.111  
  36.112  fun unparse_t t_to_ast prt_t markup ctxt t =
  36.113    let
  36.114 -    val syn = ProofContext.syn_of ctxt;
  36.115 +    val syn = Proof_Context.syn_of ctxt;
  36.116  
  36.117      fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
  36.118        | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
  36.119 @@ -620,9 +620,9 @@
  36.120          SOME "" => ([], c)
  36.121        | SOME b => markup_extern b
  36.122        | NONE => c |> Lexicon.unmark
  36.123 -         {case_class = fn x => ([Markup.tclass x], ProofContext.extern_class ctxt x),
  36.124 -          case_type = fn x => ([Markup.tycon x], ProofContext.extern_type ctxt x),
  36.125 -          case_const = fn x => ([Markup.const x], ProofContext.extern_const ctxt x),
  36.126 +         {case_class = fn x => ([Markup.tclass x], Proof_Context.extern_class ctxt x),
  36.127 +          case_type = fn x => ([Markup.tycon x], Proof_Context.extern_type ctxt x),
  36.128 +          case_const = fn x => ([Markup.const x], Proof_Context.extern_const ctxt x),
  36.129            case_fixed = fn x => free_or_skolem ctxt x,
  36.130            case_default = fn x => ([], x)});
  36.131    in
  36.132 @@ -639,9 +639,9 @@
  36.133  
  36.134  fun unparse_term ctxt =
  36.135    let
  36.136 -    val thy = ProofContext.theory_of ctxt;
  36.137 -    val syn = ProofContext.syn_of ctxt;
  36.138 -    val idents = Local_Syntax.idents_of (ProofContext.syntax_of ctxt);
  36.139 +    val thy = Proof_Context.theory_of ctxt;
  36.140 +    val syn = Proof_Context.syn_of ctxt;
  36.141 +    val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
  36.142    in
  36.143      unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
  36.144        (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
  36.145 @@ -681,7 +681,7 @@
  36.146  
  36.147  fun const_ast_tr intern ctxt [Ast.Variable c] =
  36.148        let
  36.149 -        val Const (c', _) = ProofContext.read_const_proper ctxt false c;
  36.150 +        val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
  36.151          val d = if intern then Lexicon.mark_const c' else c;
  36.152        in Ast.Constant d end
  36.153    | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T]] =
    37.1 --- a/src/Pure/Thy/term_style.ML	Sat Apr 16 15:25:25 2011 +0200
    37.2 +++ b/src/Pure/Thy/term_style.ML	Sat Apr 16 15:47:52 2011 +0200
    37.3 @@ -45,7 +45,7 @@
    37.4  
    37.5  fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse)
    37.6    >> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
    37.7 -       (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
    37.8 +       (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
    37.9           (Args.src x) ctxt |>> (fn f => f ctxt)));
   37.10  
   37.11  val parse = Args.context :|-- (fn ctxt => Scan.lift 
   37.12 @@ -56,7 +56,7 @@
   37.13  val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style.";
   37.14    Scan.lift Args.liberal_name
   37.15    >> (fn name => fst (Args.context_syntax "style"
   37.16 -       (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
   37.17 +       (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
   37.18            (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))));
   37.19  
   37.20  
   37.21 @@ -65,7 +65,7 @@
   37.22  fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
   37.23    let
   37.24      val concl =
   37.25 -      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
   37.26 +      Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
   37.27    in
   37.28      case concl of (_ $ l $ r) => proj (l, r)
   37.29      | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
    38.1 --- a/src/Pure/Thy/thy_output.ML	Sat Apr 16 15:25:25 2011 +0200
    38.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Apr 16 15:47:52 2011 +0200
    38.3 @@ -491,35 +491,35 @@
    38.4  
    38.5  fun pretty_const ctxt c =
    38.6    let
    38.7 -    val t = Const (c, Consts.type_scheme (ProofContext.consts_of ctxt) c)
    38.8 +    val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
    38.9        handle TYPE (msg, _, _) => error msg;
   38.10      val ([t'], _) = Variable.import_terms true [t] ctxt;
   38.11    in pretty_term ctxt t' end;
   38.12  
   38.13  fun pretty_abbrev ctxt s =
   38.14    let
   38.15 -    val t = Syntax.parse_term ctxt s |> singleton (ProofContext.standard_infer_types ctxt);
   38.16 +    val t = Syntax.parse_term ctxt s |> singleton (Proof_Context.standard_infer_types ctxt);
   38.17      fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
   38.18      val (head, args) = Term.strip_comb t;
   38.19      val (c, T) = Term.dest_Const head handle TERM _ => err ();
   38.20 -    val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
   38.21 +    val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
   38.22        handle TYPE _ => err ();
   38.23      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
   38.24      val eq = Logic.mk_equals (t, t');
   38.25      val ctxt' = Variable.auto_fixes eq ctxt;
   38.26 -  in ProofContext.pretty_term_abbrev ctxt' eq end;
   38.27 +  in Proof_Context.pretty_term_abbrev ctxt' eq end;
   38.28  
   38.29  fun pretty_class ctxt =
   38.30 -  Pretty.str o ProofContext.extern_class ctxt o ProofContext.read_class ctxt;
   38.31 +  Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
   38.32  
   38.33  fun pretty_type ctxt s =
   38.34 -  let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
   38.35 -  in Pretty.str (ProofContext.extern_type ctxt name) end;
   38.36 +  let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
   38.37 +  in Pretty.str (Proof_Context.extern_type ctxt name) end;
   38.38  
   38.39  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
   38.40  
   38.41  fun pretty_theory ctxt name =
   38.42 -  (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
   38.43 +  (Theory.requires (Proof_Context.theory_of ctxt) name "presentation"; Pretty.str name);
   38.44  
   38.45  
   38.46  (* default output *)
    39.1 --- a/src/Pure/Tools/find_consts.ML	Sat Apr 16 15:25:25 2011 +0200
    39.2 +++ b/src/Pure/Tools/find_consts.ML	Sat Apr 16 15:47:52 2011 +0200
    39.3 @@ -71,7 +71,7 @@
    39.4    let
    39.5      val start = Timing.start ();
    39.6  
    39.7 -    val thy = ProofContext.theory_of ctxt;
    39.8 +    val thy = Proof_Context.theory_of ctxt;
    39.9      val low_ranking = 10000;
   39.10  
   39.11      fun user_visible consts (nm, _) =
   39.12 @@ -82,7 +82,7 @@
   39.13          val raw_T = Syntax.parse_typ ctxt crit;
   39.14          val t =
   39.15            Syntax.check_term
   39.16 -            (ProofContext.set_mode ProofContext.mode_pattern ctxt)
   39.17 +            (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
   39.18              (Term.dummy_pattern raw_T);
   39.19        in Term.type_of t end;
   39.20  
    40.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Apr 16 15:25:25 2011 +0200
    40.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 16 15:47:52 2011 +0200
    40.3 @@ -43,15 +43,15 @@
    40.4  
    40.5  fun parse_pattern ctxt nm =
    40.6    let
    40.7 -    val consts = ProofContext.consts_of ctxt;
    40.8 +    val consts = Proof_Context.consts_of ctxt;
    40.9      val nm' =
   40.10        (case Syntax.parse_term ctxt nm of
   40.11          Const (c, _) => c
   40.12        | _ => Consts.intern consts nm);
   40.13    in
   40.14      (case try (Consts.the_abbreviation consts) nm' of
   40.15 -      SOME (_, rhs) => apply_dummies (ProofContext.expand_abbrevs ctxt rhs)
   40.16 -    | NONE => ProofContext.read_term_pattern ctxt nm)
   40.17 +      SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs)
   40.18 +    | NONE => Proof_Context.read_term_pattern ctxt nm)
   40.19    end;
   40.20  
   40.21  fun read_criterion _ (Name name) = Name name
   40.22 @@ -60,7 +60,7 @@
   40.23    | read_criterion _ Elim = Elim
   40.24    | read_criterion _ Dest = Dest
   40.25    | read_criterion _ Solves = Solves
   40.26 -  | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str)
   40.27 +  | read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str)
   40.28    | read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str);
   40.29  
   40.30  fun pretty_criterion ctxt (b, c) =
   40.31 @@ -131,7 +131,7 @@
   40.32    returns: smallest substitution size*)
   40.33  fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
   40.34    let
   40.35 -    val thy = ProofContext.theory_of ctxt;
   40.36 +    val thy = Proof_Context.theory_of ctxt;
   40.37  
   40.38      fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
   40.39      fun matches pat =
   40.40 @@ -216,7 +216,7 @@
   40.41      in
   40.42        (*elim rules always have assumptions, so an elim with one
   40.43          assumption is as good as an intro rule with none*)
   40.44 -      if is_nontrivial (ProofContext.theory_of ctxt) (major_prem_of theorem)
   40.45 +      if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem)
   40.46          andalso not (null successful)
   40.47        then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
   40.48      end
   40.49 @@ -274,7 +274,7 @@
   40.50      fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
   40.51        | check (theorem, c as SOME thm_consts) =
   40.52           (if subset (op =) (pat_consts, thm_consts) andalso
   40.53 -            Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, prop_of theorem)
   40.54 +            Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
   40.55            then SOME (0, 0) else NONE, c);
   40.56    in check end;
   40.57  
   40.58 @@ -378,7 +378,7 @@
   40.59  fun nicer_shortest ctxt =
   40.60    let
   40.61      (* FIXME global name space!? *)
   40.62 -    val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
   40.63 +    val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
   40.64  
   40.65      val shorten =
   40.66        Name_Space.extern
   40.67 @@ -412,10 +412,10 @@
   40.68        |> filter_out (Facts.is_concealed facts o #1);
   40.69    in
   40.70      maps Facts.selections
   40.71 -     (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
   40.72 +     (visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @
   40.73  
   40.74  
   40.75 -      visible_facts (ProofContext.facts_of ctxt))
   40.76 +      visible_facts (Proof_Context.facts_of ctxt))
   40.77    end;
   40.78  
   40.79  val limit = Unsynchronized.ref 40;
   40.80 @@ -423,7 +423,7 @@
   40.81  fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
   40.82    let
   40.83      val assms =
   40.84 -      ProofContext.get_fact ctxt (Facts.named "local.assms")
   40.85 +      Proof_Context.get_fact ctxt (Facts.named "local.assms")
   40.86          handle ERROR _ => [];
   40.87      val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
   40.88      val opt_goal' = Option.map add_prems opt_goal;
    41.1 --- a/src/Pure/axclass.ML	Sat Apr 16 15:25:25 2011 +0200
    41.2 +++ b/src/Pure/axclass.ML	Sat Apr 16 15:47:52 2011 +0200
    41.3 @@ -198,7 +198,7 @@
    41.4    (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
    41.5      SOME thm => thm
    41.6    | NONE => error ("Unproven class relation " ^
    41.7 -      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));  (* FIXME stale thy (!?) *)
    41.8 +      Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2]));  (* FIXME stale thy (!?) *)
    41.9  
   41.10  fun put_trancl_classrel ((c1, c2), th) thy =
   41.11    let
   41.12 @@ -245,7 +245,7 @@
   41.13    (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
   41.14      SOME (thm, _) => thm
   41.15    | NONE => error ("Unproven type arity " ^
   41.16 -      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));  (* FIXME stale thy (!?) *)
   41.17 +      Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));  (* FIXME stale thy (!?) *)
   41.18  
   41.19  fun thynames_of_arity thy (c, a) =
   41.20    Symtab.lookup_list (proven_arities_of thy) a
   41.21 @@ -359,7 +359,7 @@
   41.22    in (c1, c2) end;
   41.23  
   41.24  fun read_classrel thy raw_rel =
   41.25 -  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel)
   41.26 +  cert_classrel thy (pairself (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel)
   41.27      handle TYPE (msg, _, _) => error msg;
   41.28  
   41.29  
   41.30 @@ -464,7 +464,7 @@
   41.31  
   41.32  fun prove_classrel raw_rel tac thy =
   41.33    let
   41.34 -    val ctxt = ProofContext.init_global thy;
   41.35 +    val ctxt = Proof_Context.init_global thy;
   41.36      val (c1, c2) = cert_classrel thy raw_rel;
   41.37      val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
   41.38        cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
   41.39 @@ -475,8 +475,8 @@
   41.40  
   41.41  fun prove_arity raw_arity tac thy =
   41.42    let
   41.43 -    val ctxt = ProofContext.init_global thy;
   41.44 -    val arity = ProofContext.cert_arity ctxt raw_arity;
   41.45 +    val ctxt = Proof_Context.init_global thy;
   41.46 +    val arity = Proof_Context.cert_arity ctxt raw_arity;
   41.47      val names = map (prefix arity_prefix) (Logic.name_arities arity);
   41.48      val props = Logic.mk_arities arity;
   41.49      val ths = Goal.prove_multi ctxt [] [] props
   41.50 @@ -617,7 +617,7 @@
   41.51      (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
   41.52  
   41.53  fun ax_arity prep =
   41.54 -  axiomatize (prep o ProofContext.init_global) Logic.mk_arities
   41.55 +  axiomatize (prep o Proof_Context.init_global) Logic.mk_arities
   41.56      (map (prefix arity_prefix) o Logic.name_arities) add_arity;
   41.57  
   41.58  fun class_const c =
   41.59 @@ -637,11 +637,11 @@
   41.60  in
   41.61  
   41.62  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
   41.63 -val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
   41.64 +val axiomatize_class_cmd = ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
   41.65  val axiomatize_classrel = ax_classrel cert_classrel;
   41.66  val axiomatize_classrel_cmd = ax_classrel read_classrel;
   41.67 -val axiomatize_arity = ax_arity ProofContext.cert_arity;
   41.68 -val axiomatize_arity_cmd = ax_arity ProofContext.read_arity;
   41.69 +val axiomatize_arity = ax_arity Proof_Context.cert_arity;
   41.70 +val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity;
   41.71  
   41.72  end;
   41.73  
    42.1 --- a/src/Pure/codegen.ML	Sat Apr 16 15:25:25 2011 +0200
    42.2 +++ b/src/Pure/codegen.ML	Sat Apr 16 15:47:52 2011 +0200
    42.3 @@ -821,7 +821,7 @@
    42.4  
    42.5  val generate_code_i = gen_generate_code Sign.cert_term;
    42.6  val generate_code =
    42.7 -  gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init_global);
    42.8 +  gen_generate_code (Syntax.read_term o Proof_Context.allow_dummies o Proof_Context.init_global);
    42.9  
   42.10  
   42.11  (**** Reflection ****)
   42.12 @@ -872,7 +872,7 @@
   42.13  
   42.14  fun test_term ctxt t =
   42.15    let
   42.16 -    val thy = ProofContext.theory_of ctxt;
   42.17 +    val thy = Proof_Context.theory_of ctxt;
   42.18      val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
   42.19        (generate_code_i thy [] "Generated") [("testf", t)];
   42.20      val Ts = map snd (fst (strip_abs t));
   42.21 @@ -906,7 +906,7 @@
   42.22  
   42.23  fun eval_term thy t =
   42.24    let
   42.25 -    val ctxt = ProofContext.init_global thy;  (* FIXME *)
   42.26 +    val ctxt = Proof_Context.init_global thy;  (* FIXME *)
   42.27      val e =
   42.28        let
   42.29          val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    43.1 --- a/src/Pure/context.ML	Sat Apr 16 15:25:25 2011 +0200
    43.2 +++ b/src/Pure/context.ML	Sat Apr 16 15:47:52 2011 +0200
    43.3 @@ -17,7 +17,7 @@
    43.4    type theory_ref
    43.5    exception THEORY of string * theory list
    43.6    structure Proof: sig type context end
    43.7 -  structure ProofContext:
    43.8 +  structure Proof_Context:
    43.9    sig
   43.10      val theory_of: Proof.context -> theory
   43.11      val init_global: theory -> Proof.context
   43.12 @@ -492,7 +492,7 @@
   43.13      val thy_ref' = check_thy thy';
   43.14    in Proof.Context (data', thy_ref') end;
   43.15  
   43.16 -structure ProofContext =
   43.17 +structure Proof_Context =
   43.18  struct
   43.19    val theory_of = theory_of_proof;
   43.20    fun init_global thy = Proof.Context (init_data thy, check_thy thy);
   43.21 @@ -510,7 +510,7 @@
   43.22  fun get k dest prf =
   43.23    dest (case Datatab.lookup (data_of_proof prf) k of
   43.24      SOME x => x
   43.25 -  | NONE => invoke_init k (ProofContext.theory_of prf));   (*adhoc value*)
   43.26 +  | NONE => invoke_init k (Proof_Context.theory_of prf));   (*adhoc value*)
   43.27  
   43.28  fun put k mk x = map_prf (Datatab.update (k, mk x));
   43.29  
   43.30 @@ -542,8 +542,8 @@
   43.31  fun theory_map f = the_theory o f o Theory;
   43.32  fun proof_map f = the_proof o f o Proof;
   43.33  
   43.34 -val theory_of = cases I ProofContext.theory_of;
   43.35 -val proof_of = cases ProofContext.init_global I;
   43.36 +val theory_of = cases I Proof_Context.theory_of;
   43.37 +val proof_of = cases Proof_Context.init_global I;
   43.38  
   43.39  
   43.40  
    44.1 --- a/src/Pure/goal.ML	Sat Apr 16 15:25:25 2011 +0200
    44.2 +++ b/src/Pure/goal.ML	Sat Apr 16 15:47:52 2011 +0200
    44.3 @@ -154,7 +154,7 @@
    44.4  
    44.5  fun future_result ctxt result prop =
    44.6    let
    44.7 -    val thy = ProofContext.theory_of ctxt;
    44.8 +    val thy = Proof_Context.theory_of ctxt;
    44.9      val _ = Context.reject_draft thy;
   44.10      val cert = Thm.cterm_of thy;
   44.11      val certT = Thm.ctyp_of thy;
   44.12 @@ -203,7 +203,7 @@
   44.13  
   44.14  fun prove_common immediate ctxt xs asms props tac =
   44.15    let
   44.16 -    val thy = ProofContext.theory_of ctxt;
   44.17 +    val thy = Proof_Context.theory_of ctxt;
   44.18      val string_of_term = Syntax.string_of_term ctxt;
   44.19  
   44.20      val pos = Position.thread_data ();
   44.21 @@ -252,7 +252,7 @@
   44.22  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
   44.23  
   44.24  fun prove_global thy xs asms prop tac =
   44.25 -  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
   44.26 +  Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
   44.27  
   44.28  
   44.29  
    45.1 --- a/src/Pure/pure_setup.ML	Sat Apr 16 15:25:25 2011 +0200
    45.2 +++ b/src/Pure/pure_setup.ML	Sat Apr 16 15:47:52 2011 +0200
    45.3 @@ -56,3 +56,7 @@
    45.4  val cd = File.cd o Path.explode;
    45.5  
    45.6  Proofterm.proofs := 0;
    45.7 +
    45.8 +(*legacy*)
    45.9 +structure ProofContext = Proof_Context;
   45.10 +
    46.1 --- a/src/Pure/raw_simplifier.ML	Sat Apr 16 15:25:25 2011 +0200
    46.2 +++ b/src/Pure/raw_simplifier.ML	Sat Apr 16 15:47:52 2011 +0200
    46.3 @@ -316,7 +316,7 @@
    46.4  in
    46.5  
    46.6  fun print_term_global ss warn a thy t =
    46.7 -  print_term ss warn (K a) t (ProofContext.init_global thy);
    46.8 +  print_term ss warn (K a) t (Proof_Context.init_global thy);
    46.9  
   46.10  fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
   46.11  fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
   46.12 @@ -365,13 +365,13 @@
   46.13  fun context ctxt =
   46.14    map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
   46.15  
   46.16 -val global_context = context o ProofContext.init_global;
   46.17 +val global_context = context o Proof_Context.init_global;
   46.18  
   46.19  fun activate_context thy ss =
   46.20    let
   46.21      val ctxt = the_context ss;
   46.22      val ctxt' = ctxt
   46.23 -      |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
   46.24 +      |> Context.raw_transfer (Theory.merge (thy, Proof_Context.theory_of ctxt))
   46.25        |> Context_Position.set_visible false;
   46.26    in context ctxt' ss end;
   46.27  
   46.28 @@ -639,7 +639,7 @@
   46.29  
   46.30  fun mk_simproc name lhss proc =
   46.31    make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
   46.32 -    proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
   46.33 +    proc (Proof_Context.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
   46.34  
   46.35  (* FIXME avoid global thy and Logic.varify_global *)
   46.36  fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
    47.1 --- a/src/Pure/sign.ML	Sat Apr 16 15:25:25 2011 +0200
    47.2 +++ b/src/Pure/sign.ML	Sat Apr 16 15:47:52 2011 +0200
    47.3 @@ -350,7 +350,7 @@
    47.4  
    47.5  fun gen_syntax change_gram parse_typ mode args thy =
    47.6    let
    47.7 -    val ctxt = ProofContext.init_global thy;
    47.8 +    val ctxt = Proof_Context.init_global thy;
    47.9      fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
   47.10        handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
   47.11    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
   47.12 @@ -387,7 +387,7 @@
   47.13  
   47.14  fun gen_add_consts parse_typ raw_args thy =
   47.15    let
   47.16 -    val ctxt = ProofContext.init_global thy;
   47.17 +    val ctxt = Proof_Context.init_global thy;
   47.18      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
   47.19      fun prep (b, raw_T, mx) =
   47.20        let
    48.1 --- a/src/Pure/simplifier.ML	Sat Apr 16 15:25:25 2011 +0200
    48.2 +++ b/src/Pure/simplifier.ML	Sat Apr 16 15:47:52 2011 +0200
    48.3 @@ -132,7 +132,7 @@
    48.4  fun map_simpset f = Context.theory_map (map_ss f);
    48.5  fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
    48.6  fun global_simpset_of thy =
    48.7 -  Raw_Simplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
    48.8 +  Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
    48.9  
   48.10  fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   48.11  fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
   48.12 @@ -193,7 +193,7 @@
   48.13              |> fold Variable.declare_term lhss'
   48.14              |> fold Variable.auto_fixes lhss';
   48.15          in Variable.export_terms ctxt' lthy lhss' end
   48.16 -        |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
   48.17 +        |> map (Thm.cterm_of (Proof_Context.theory_of lthy)),
   48.18         proc = proc,
   48.19         identifier = identifier};
   48.20    in
    49.1 --- a/src/Pure/subgoal.ML	Sat Apr 16 15:25:25 2011 +0200
    49.2 +++ b/src/Pure/subgoal.ML	Sat Apr 16 15:47:52 2011 +0200
    49.3 @@ -67,7 +67,7 @@
    49.4  *)
    49.5  fun lift_import idx params th ctxt =
    49.6    let
    49.7 -    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
    49.8 +    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    49.9      val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
   49.10  
   49.11      val Ts = map (#T o Thm.rep_cterm) params;
    50.1 --- a/src/Pure/theory.ML	Sat Apr 16 15:25:25 2011 +0200
    50.2 +++ b/src/Pure/theory.ML	Sat Apr 16 15:47:52 2011 +0200
    50.3 @@ -240,7 +240,7 @@
    50.4  
    50.5  fun check_def thy unchecked overloaded (b, tm) defs =
    50.6    let
    50.7 -    val ctxt = ProofContext.init_global thy;
    50.8 +    val ctxt = Proof_Context.init_global thy;
    50.9      val name = Sign.full_name thy b;
   50.10      val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
   50.11        handle TERM (msg, _) => error msg;
    51.1 --- a/src/Pure/thm.ML	Sat Apr 16 15:25:25 2011 +0200
    51.2 +++ b/src/Pure/thm.ML	Sat Apr 16 15:47:52 2011 +0200
    51.3 @@ -1735,7 +1735,7 @@
    51.4  );
    51.5  
    51.6  fun extern_oracles ctxt =
    51.7 -  map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt)));
    51.8 +  map #1 (Name_Space.extern_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
    51.9  
   51.10  fun add_oracle (b, oracle) thy =
   51.11    let
    52.1 --- a/src/Pure/type_infer.ML	Sat Apr 16 15:25:25 2011 +0200
    52.2 +++ b/src/Pure/type_infer.ML	Sat Apr 16 15:47:52 2011 +0200
    52.3 @@ -219,7 +219,7 @@
    52.4  
    52.5  fun unify ctxt pp =
    52.6    let
    52.7 -    val thy = ProofContext.theory_of ctxt;
    52.8 +    val thy = Proof_Context.theory_of ctxt;
    52.9      val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
   52.10  
   52.11  
    53.1 --- a/src/Pure/variable.ML	Sat Apr 16 15:25:25 2011 +0200
    53.2 +++ b/src/Pure/variable.ML	Sat Apr 16 15:47:52 2011 +0200
    53.3 @@ -239,7 +239,7 @@
    53.4  val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
    53.5  
    53.6  val declare_thm = Thm.fold_terms declare_internal;
    53.7 -fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th));
    53.8 +fun global_thm_context th = declare_thm th (Proof_Context.init_global (Thm.theory_of_thm th));
    53.9  
   53.10  
   53.11  (* renaming term/type frees *)
   53.12 @@ -430,7 +430,7 @@
   53.13  
   53.14  fun importT ths ctxt =
   53.15    let
   53.16 -    val thy = ProofContext.theory_of ctxt;
   53.17 +    val thy = Proof_Context.theory_of ctxt;
   53.18      val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
   53.19      val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
   53.20      val ths' = map (Thm.instantiate insts') ths;
   53.21 @@ -444,7 +444,7 @@
   53.22  
   53.23  fun import is_open ths ctxt =
   53.24    let
   53.25 -    val thy = ProofContext.theory_of ctxt;
   53.26 +    val thy = Proof_Context.theory_of ctxt;
   53.27      val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
   53.28      val insts' = Thm.certify_inst thy insts;
   53.29      val ths' = map (Thm.instantiate insts') ths;