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;