--- a/NEWS Sat Apr 16 15:25:25 2011 +0200
+++ b/NEWS Sat Apr 16 15:47:52 2011 +0200
@@ -84,6 +84,9 @@
*** ML ***
+* Structure Proof_Context follows standard naming scheme. Old
+ProofContext is still available for some time as legacy alias.
+
* Structure Timing provides various operations for timing; supersedes
former start_timing/end_timing etc.
--- a/src/Pure/Isar/args.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/args.ML Sat Apr 16 15:47:52 2011 +0200
@@ -184,25 +184,25 @@
(* terms and types *)
-val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
+val typ_abbrev = Scan.peek (named_typ o Proof_Context.read_typ_abbrev o Context.proof_of);
val typ = Scan.peek (named_typ o Syntax.read_typ o Context.proof_of);
val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of);
-val term_abbrev = Scan.peek (named_term o ProofContext.read_term_abbrev o Context.proof_of);
+val term_abbrev = Scan.peek (named_term o Proof_Context.read_term_abbrev o Context.proof_of);
val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of);
(* type and constant names *)
fun type_name strict =
- Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict))
+ Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) strict))
>> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
fun const strict =
- Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict dummyT))
+ Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) strict dummyT))
>> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
fun const_proper strict =
- Scan.peek (fn ctxt => named_term (ProofContext.read_const_proper (Context.proof_of ctxt) strict))
+ Scan.peek (fn ctxt => named_term (Proof_Context.read_const_proper (Context.proof_of ctxt) strict))
>> (fn Const (c, _) => c | _ => "");
--- a/src/Pure/Isar/attrib.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Sat Apr 16 15:47:52 2011 +0200
@@ -73,7 +73,7 @@
fun print_attributes thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
val attribs = Attributes.get thy;
fun prt_attr (name, (_, comment)) = Pretty.block
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
@@ -91,7 +91,7 @@
val intern = Name_Space.intern o #1 o Attributes.get;
val intern_src = Args.map_name o intern;
-fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (ProofContext.theory_of ctxt)));
+fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (Proof_Context.theory_of ctxt)));
(* pretty printing *)
@@ -130,8 +130,8 @@
(* fact expressions *)
fun eval_thms ctxt srcs = ctxt
- |> ProofContext.note_thmss ""
- (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
+ |> Proof_Context.note_thmss ""
+ (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt)
[((Binding.empty, []), srcs)])
|> fst |> maps snd;
@@ -143,7 +143,7 @@
thm structure.*)
fun crude_closure ctxt src =
- (try (fn () => attribute_i (ProofContext.theory_of ctxt) src
+ (try (fn () => attribute_i (Proof_Context.theory_of ctxt) src
(Context.Proof ctxt, Drule.asm_rl)) ();
Args.closure src);
@@ -185,7 +185,7 @@
fun gen_thm pick = Scan.depend (fn context =>
let
val thy = Context.theory_of context;
- val get = Context.cases (Global_Theory.get_fact context) ProofContext.get_fact context;
+ val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
val get_fact = get o Facts.Fact;
fun get_named pos name = get (Facts.Named ((name, pos), NONE));
in
@@ -336,7 +336,7 @@
fun print_configs ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
fun prt (name, config) =
let val value = Config.get ctxt config in
Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
@@ -413,7 +413,7 @@
register_config Name_Space.short_names_raw #>
register_config Name_Space.unique_names_raw #>
register_config ML_Context.trace_raw #>
- register_config ProofContext.show_abbrevs_raw #>
+ register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
register_config Goal_Display.show_consts_raw #>
--- a/src/Pure/Isar/calculation.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/calculation.ML Sat Apr 16 15:47:52 2011 +0200
@@ -116,8 +116,8 @@
val _ =
if int then
Pretty.writeln
- (ProofContext.pretty_fact ctxt'
- (ProofContext.full_name ctxt' (Binding.name calculationN), calc))
+ (Proof_Context.pretty_fact ctxt'
+ (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
else ();
in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
--- a/src/Pure/Isar/class.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/class.ML Sat Apr 16 15:47:52 2011 +0200
@@ -151,7 +151,7 @@
fun print_classes ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val algebra = Sign.classes_of thy;
val arities =
Symtab.empty
@@ -164,10 +164,10 @@
val Ss = Sorts.mg_domain algebra tyco [class];
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
fun mk_param (c, ty) =
- Pretty.str (ProofContext.extern_const ctxt c ^ " :: " ^
+ Pretty.str (Proof_Context.extern_const ctxt c ^ " :: " ^
Syntax.string_of_typ (Config.put show_sorts false ctxt) (Type.strip_sorts ty));
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
- (SOME o Pretty.str) ("class " ^ ProofContext.extern_class ctxt class ^ ":"),
+ (SOME o Pretty.str) ("class " ^ Proof_Context.extern_class ctxt class ^ ":"),
(SOME o Pretty.block) [Pretty.str "supersort: ",
(Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
@@ -257,7 +257,7 @@
fun synchronize_class_syntax sort base_sort ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val algebra = Sign.classes_of thy;
val operations = these_operations thy sort;
fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
@@ -310,7 +310,7 @@
lthy
|> Local_Theory.raw_theory f
|> Local_Theory.target (synchronize_class_syntax [class]
- (base_sort (ProofContext.theory_of lthy) class));
+ (base_sort (Proof_Context.theory_of lthy) class));
local
@@ -369,10 +369,10 @@
fun gen_classrel mk_prop classrel thy =
let
fun after_qed results =
- ProofContext.background_theory ((fold o fold) AxClass.add_classrel results);
+ Proof_Context.background_theory ((fold o fold) AxClass.add_classrel results);
in
thy
- |> ProofContext.init_global
+ |> Proof_Context.init_global
|> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
end;
@@ -421,8 +421,8 @@
fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
let
- val ctxt = ProofContext.init_global thy;
- val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
+ val ctxt = Proof_Context.init_global thy;
+ val all_arities = map (fn raw_tyco => Proof_Context.read_arity ctxt
(raw_tyco, raw_sorts, raw_sort)) raw_tycos;
val tycos = map #1 all_arities;
val (_, sorts, sort) = hd all_arities;
@@ -437,7 +437,7 @@
val Instantiation { params, ... } = Instantiation.get ctxt;
val lookup_inst_param = AxClass.lookup_inst_param
- (Sign.consts_of (ProofContext.theory_of ctxt)) params;
+ (Sign.consts_of (Proof_Context.theory_of ctxt)) params;
fun subst (c, ty) = case lookup_inst_param (c, ty)
of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
| NONE => NONE;
@@ -498,23 +498,23 @@
fun pretty lthy =
let
val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
fun pr_param ((c, _), (v, ty)) =
Pretty.block (Pretty.breaks
- [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
+ [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
Pretty.str "::", Syntax.pretty_typ lthy ty]);
in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
fun conclude lthy =
let
val (tycos, vs, sort) = #arities (the_instantiation lthy);
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
val _ = tycos |> List.app (fn tyco =>
if Sign.of_sort thy
(Type (tyco, map TFree vs), sort)
then ()
- else error ("Missing instance proof for type " ^ quote (ProofContext.extern_type lthy tyco)));
+ else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco)));
in lthy end;
fun instantiation (tycos, vs, sort) thy =
@@ -545,7 +545,7 @@
in
thy
|> Theory.checkpoint
- |> ProofContext.init_global
+ |> Proof_Context.init_global
|> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
|> fold (Variable.declare_typ o TFree) vs
|> fold (Variable.declare_names o Free o snd) params
@@ -593,8 +593,8 @@
fun prove_instantiation_exit_result f tac x lthy =
let
- val morph = ProofContext.export_morphism lthy
- (ProofContext.init_global (ProofContext.theory_of lthy));
+ val morph = Proof_Context.export_morphism lthy
+ (Proof_Context.init_global (Proof_Context.theory_of lthy));
val y = f morph x;
in
lthy
@@ -610,11 +610,11 @@
val (tycos, vs, sort) = read_multi_arity thy raw_arities;
val sorts = map snd vs;
val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
- fun after_qed results = ProofContext.background_theory
+ fun after_qed results = Proof_Context.background_theory
((fold o fold) AxClass.add_arity results);
in
thy
- |> ProofContext.init_global
+ |> Proof_Context.init_global
|> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
end;
--- a/src/Pure/Isar/class_declaration.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML Sat Apr 16 15:47:52 2011 +0200
@@ -27,7 +27,7 @@
fun calculate thy class sups base_sort param_map assm_axiom =
let
- val empty_ctxt = ProofContext.init_global thy;
+ val empty_ctxt = Proof_Context.init_global thy;
(* instantiation of canonical interpretation *)
val aT = TFree (Name.aT, base_sort);
@@ -55,7 +55,7 @@
of (_, NONE) => all_tac
| (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
val tac = loc_intro_tac
- THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
+ THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom))
in Element.prove_witness empty_ctxt prop tac end) prop;
val axiom = Option.map Element.conclude_witness wit;
@@ -73,7 +73,7 @@
of SOME eq_morph => const_morph $> eq_morph
| NONE => const_morph
val thm'' = Morphism.thm const_eq_morph thm';
- val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
+ val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
val assm_intro = Option.map prove_assm_intro
(fst (Locale.intros_of thy class));
@@ -146,11 +146,11 @@
(* preprocessing elements, retrieving base sort from type-checked elements *)
val raw_supexpr = (map (fn sup => (sup, (("", false),
Expression.Positional []))) sups, []);
- val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
+ val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
#> Class.redeclare_operations thy sups
#> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
#> add_typ_check ~10 "singleton_fixate" singleton_fixate;
- val ((raw_supparams, _, raw_inferred_elems), _) = ProofContext.init_global thy
+ val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
|> add_typ_check 5 "after_infer_fixate" after_infer_fixate
|> prep_decl raw_supexpr init_class_body raw_elems;
fun filter_element (Element.Fixes []) = NONE
@@ -207,7 +207,7 @@
val sup_sort = inter_sort base_sort sups;
(* process elements as class specification *)
- val class_ctxt = Class.begin sups base_sort (ProofContext.init_global thy);
+ val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
val ((_, _, syntax_elems), _) = class_ctxt
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs = if null vs
@@ -324,7 +324,7 @@
fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
let
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
val proto_sup = prep_class thy raw_sup;
val proto_sub = case Named_Target.peek lthy
of SOME {target, is_class = true, ...} => target
@@ -337,9 +337,9 @@
val some_prop = try the_single props;
val some_dep_morph = try the_single (map snd deps);
fun after_qed some_wit =
- ProofContext.background_theory (Class.register_subclass (sub, sup)
+ Proof_Context.background_theory (Class.register_subclass (sub, sup)
some_dep_morph some_wit export)
- #> ProofContext.theory_of #> Named_Target.init before_exit sub;
+ #> Proof_Context.theory_of #> Named_Target.init before_exit sub;
in do_proof after_qed some_prop goal_ctxt end;
fun user_proof after_qed some_prop =
@@ -354,7 +354,7 @@
val subclass = gen_subclass (K I) user_proof;
fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
-val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
+val subclass_cmd = gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof;
end; (*local*)
--- a/src/Pure/Isar/code.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/code.ML Sat Apr 16 15:47:52 2011 +0200
@@ -113,12 +113,12 @@
Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
fun string_of_const thy c =
- let val ctxt = ProofContext.init_global thy in
+ let val ctxt = Proof_Context.init_global thy in
case AxClass.inst_of_param thy c of
SOME (c, tyco) =>
- ProofContext.extern_const ctxt c ^ " " ^ enclose "[" "]"
- (ProofContext.extern_type ctxt tyco)
- | NONE => ProofContext.extern_const ctxt c
+ Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]"
+ (Proof_Context.extern_type ctxt tyco)
+ | NONE => Proof_Context.extern_const ctxt c
end;
@@ -353,7 +353,7 @@
fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
fun read_signature thy = cert_signature thy o Type.strip_sorts
- o Syntax.parse_typ (ProofContext.init_global thy);
+ o Syntax.parse_typ (Proof_Context.init_global thy);
fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
@@ -576,7 +576,7 @@
fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
-fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy);
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
apfst (meta_rewrite thy);
@@ -963,7 +963,7 @@
fun print_codesetup thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
val exec = the_exec thy;
fun pretty_equations const thms =
(Pretty.block o Pretty.fbreaks) (
@@ -1150,7 +1150,7 @@
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
- THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
+ THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
fun add_case thm thy =
--- a/src/Pure/Isar/element.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/element.ML Sat Apr 16 15:47:52 2011 +0200
@@ -222,7 +222,7 @@
fun obtain prop ctxt =
let
val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
- fun fix (x, T) = (Binding.name (ProofContext.revert_skolem ctxt' x), SOME T);
+ fun fix (x, T) = (Binding.name (Proof_Context.revert_skolem ctxt' x), SOME T);
val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
val As = Logic.strip_imp_prems (Thm.term_of prop');
in ((Binding.empty, (xs, As)), ctxt') end;
@@ -231,7 +231,7 @@
fun pretty_statement ctxt kind raw_th =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val cert = Thm.cterm_of thy;
val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
@@ -242,7 +242,7 @@
val fixes = fold_aterms (fn v as Free (x, T) =>
if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
- then insert (op =) (ProofContext.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
+ then insert (op =) (Proof_Context.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
val (assumes, cases) = take_suffix (fn prem =>
is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
in
@@ -295,7 +295,7 @@
fun proof_local cmd goal_ctxt int after_qed' propss =
Proof.map_context (K goal_ctxt)
- #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
+ #> Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
in
@@ -491,27 +491,27 @@
in
context |> Context.mapping_result
(Global_Theory.note_thmss kind facts')
- (ProofContext.note_thmss kind facts')
+ (Proof_Context.note_thmss kind facts')
end;
-fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
+fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
| init (Constrains _) = I
| init (Assumes asms) = Context.map_proof (fn ctxt =>
let
- val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
+ val asms' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) asms;
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (maps (map #1 o #2) asms')
- |> ProofContext.add_assms_i Assumption.assume_export asms';
+ |> Proof_Context.add_assms_i Assumption.assume_export asms';
in ctxt' end)
| init (Defines defs) = Context.map_proof (fn ctxt =>
let
- val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
+ val defs' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (map #1 asms)
- |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
+ |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
| init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
@@ -530,8 +530,8 @@
typ = I,
term = I,
pattern = I,
- fact = ProofContext.get_fact ctxt,
- attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}
+ fact = Proof_Context.get_fact ctxt,
+ attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)}
in activate_i elem ctxt end;
end;
--- a/src/Pure/Isar/expression.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/expression.ML Sat Apr 16 15:47:52 2011 +0200
@@ -185,7 +185,7 @@
val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
val inst = Symtab.make insts'';
in
- (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
+ (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
end;
@@ -198,15 +198,15 @@
Element.map_ctxt
{binding = I,
typ = prep_typ ctxt,
- term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt),
- pattern = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt),
+ term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt),
+ pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt),
fact = I,
attrib = I};
fun parse_concl prep_term ctxt concl =
(map o map) (fn (t, ps) =>
- (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t,
- map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
+ (prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
+ map (prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) concl;
(** Simultaneous type inference: instantiations + elements + conclusion **)
@@ -247,12 +247,12 @@
fun prep (_, pats) (ctxt, t :: ts) =
let val ctxt' = Variable.auto_fixes t ctxt
in
- ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
+ ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
(ctxt', ts))
end;
val (cs', (context', _)) = fold_map prep cs
(context, Syntax.check_terms
- (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
+ (Proof_Context.set_mode Proof_Context.mode_schematic context) (map fst cs));
in (cs', context') end;
in
@@ -279,7 +279,7 @@
fun declare_elem prep_vars (Fixes fixes) ctxt =
let val (vars, _) = prep_vars fixes ctxt
- in ctxt |> ProofContext.add_fixes vars |> snd end
+ in ctxt |> Proof_Context.add_fixes vars |> snd end
| declare_elem prep_vars (Constrains csts) ctxt =
ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
| declare_elem _ (Assumes _) ctxt = ctxt
@@ -322,7 +322,7 @@
fun finish_inst ctxt (loc, (prfx, inst)) =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
in (loc, morph) end;
@@ -346,7 +346,7 @@
fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
{strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
let
- val thy = ProofContext.theory_of ctxt1;
+ val thy = Proof_Context.theory_of ctxt1;
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
@@ -377,7 +377,7 @@
in check_autofix insts elems concl ctxt end;
val fors = prep_vars_inst fixed ctxt1 |> fst;
- val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
+ val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
val add_free = fold_aterms
@@ -397,7 +397,7 @@
(* Retrieve parameter types *)
val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
| _ => fn ps => ps) (Fixes fors :: elems') [];
- val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
+ val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
val parms = xs ~~ Ts; (* params from expression and elements *)
val Fixes fors' = finish_primitive parms I (Fixes fors);
@@ -409,16 +409,16 @@
in
fun cert_full_context_statement x =
- prep_full_context_statement (K I) (K I) ProofContext.cert_vars
- make_inst ProofContext.cert_vars (K I) x;
+ prep_full_context_statement (K I) (K I) Proof_Context.cert_vars
+ make_inst Proof_Context.cert_vars (K I) x;
fun cert_read_full_context_statement x =
- prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
- make_inst ProofContext.cert_vars (K I) x;
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
+ make_inst Proof_Context.cert_vars (K I) x;
fun read_full_context_statement x =
- prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
- parse_inst ProofContext.read_vars intern x;
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
+ parse_inst Proof_Context.read_vars intern x;
end;
@@ -433,7 +433,7 @@
prep {strict = true, do_close = false, fixed_frees = true}
([], []) I raw_elems raw_concl context;
val (_, context') = context |>
- ProofContext.set_stmt true |>
+ Proof_Context.set_stmt true |>
fold_map activate elems;
in (concl, context') end;
@@ -448,7 +448,7 @@
(* Locale declaration: import + elements *)
fun fix_params params =
- ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
+ Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
local
@@ -462,7 +462,7 @@
fix_params fixed |>
fold (Context.proof_map o Locale.activate_facts NONE) deps;
val (elems', _) = context' |>
- ProofContext.set_stmt true |>
+ Proof_Context.set_stmt true |>
fold_map activate elems;
in ((fixed, deps, elems'), (parms, ctxt')) end;
@@ -488,7 +488,7 @@
fun prep_goal_expression prep expression context =
let
- val thy = ProofContext.theory_of context;
+ val thy = Proof_Context.theory_of context;
val ((fixed, deps, _, _), _) =
prep {strict = true, do_close = true, fixed_frees = true} expression I [] [] context;
@@ -566,7 +566,7 @@
fun eval_inst ctxt (loc, morph) text =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val (asm, defs) = Locale.specification_of thy loc;
val asm' = Option.map (Morphism.term morph) asm;
val defs' = map (Morphism.term morph) defs;
@@ -616,7 +616,7 @@
fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
if length args = n then
Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *)
- Term.list_comb (Syntax.free (ProofContext.extern_const ctxt c), args)
+ Term.list_comb (Syntax.free (Proof_Context.extern_const ctxt c), args)
else raise Match);
(* define one predicate including its intro rule and axioms
@@ -651,7 +651,7 @@
|> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
|> Global_Theory.add_defs false
[((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
- val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
+ val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
@@ -738,7 +738,7 @@
error ("Duplicate definition of locale " ^ quote name);
val ((fixed, deps, body_elems), (parms, ctxt')) =
- prep_decl raw_import I raw_body (ProofContext.init_global thy);
+ prep_decl raw_import I raw_body (Proof_Context.init_global thy);
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
val extraTs =
@@ -825,7 +825,7 @@
fun gen_interpretation prep_expr parse_prop prep_attr
expression equations theory =
let
- val ((propss, deps, export), expr_ctxt) = ProofContext.init_global theory
+ val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global theory
|> prep_expr expression;
val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
@@ -834,7 +834,7 @@
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
fun after_qed witss eqns =
- (ProofContext.background_theory o Context.theory_map)
+ (Proof_Context.background_theory o Context.theory_map)
(note_eqns_register deps witss attrss eqns export export');
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
@@ -844,7 +844,7 @@
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
- val theory = ProofContext.theory_of ctxt;
+ val theory = Proof_Context.theory_of ctxt;
val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
@@ -891,7 +891,7 @@
in
ctxt
|> Locale.add_thmss target Thm.lemmaK facts
- |> ProofContext.background_theory (fold (fn ((dep, morph), wits) =>
+ |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
fn theory =>
Locale.add_dependency target
(dep, morph $> Element.satisfy_morphism
--- a/src/Pure/Isar/generic_target.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML Sat Apr 16 15:47:52 2011 +0200
@@ -50,8 +50,8 @@
fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
let
- val thy = ProofContext.theory_of lthy;
- val thy_ctxt = ProofContext.init_global thy;
+ val thy = Proof_Context.theory_of lthy;
+ val thy_ctxt = Proof_Context.init_global thy;
val b_def = Thm.def_binding_optional b proto_b_def;
@@ -99,8 +99,8 @@
fun import_export_proof ctxt (name, raw_th) =
let
- val thy = ProofContext.theory_of ctxt;
- val thy_ctxt = ProofContext.init_global thy;
+ val thy = Proof_Context.theory_of ctxt;
+ val thy_ctxt = Proof_Context.init_global thy;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
@@ -145,7 +145,7 @@
fun notes target_notes kind facts lthy =
let
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
val facts' = facts
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
(Local_Theory.full_name lthy (fst a))) bs))
@@ -155,7 +155,7 @@
in
lthy
|> target_notes kind global_facts local_facts
- |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
+ |> Proof_Context.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
end;
@@ -163,7 +163,7 @@
fun abbrev target_abbrev prmode ((b, mx), t) lthy =
let
- val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
+ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
val target_ctxt = Local_Theory.target_of lthy;
val t' = Assumption.export_term lthy target_ctxt t;
@@ -179,7 +179,7 @@
in
lthy
|> target_abbrev prmode (b, mx') (global_rhs, t') xs
- |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
+ |> Proof_Context.add_abbrev Print_Mode.internal (b, t) |> snd
|> Local_Defs.fixed_abbrev ((b, NoSyn), t)
end;
@@ -207,12 +207,12 @@
fun theory_notes kind global_facts lthy =
let
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
in
lthy
|> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
- |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.target (Proof_Context.note_thmss kind global_facts' #> snd)
end;
fun theory_abbrev prmode ((b, mx), t) =
--- a/src/Pure/Isar/isar_cmd.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat Apr 16 15:47:52 2011 +0200
@@ -159,10 +159,10 @@
fun read_trrules thy raw_rules =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
in
raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
- Syntax_Phases.parse_ast_pattern ctxt (ProofContext.intern_type ctxt r, s)))
+ Syntax_Phases.parse_ast_pattern ctxt (Proof_Context.intern_type ctxt r, s)))
end;
fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
@@ -326,24 +326,24 @@
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
val print_syntax = Toplevel.unknown_context o
- Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
+ Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of);
val print_abbrevs = Toplevel.unknown_context o
- Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
+ Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of);
val print_facts = Toplevel.unknown_context o
- Toplevel.keep (ProofContext.print_lthms o Toplevel.context_of);
+ Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of);
val print_configs = Toplevel.unknown_context o
Toplevel.keep (Attrib.print_configs o Toplevel.context_of);
val print_theorems_proof =
- Toplevel.keep (ProofContext.print_lthms o Proof.context_of o Toplevel.proof_of);
+ Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);
fun print_theorems_theory verbose = Toplevel.keep (fn state =>
Toplevel.theory_of state |>
(case Toplevel.previous_context_of state of
- SOME prev => Proof_Display.print_theorems_diff verbose (ProofContext.theory_of prev)
+ SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev)
| NONE => Proof_Display.print_theorems verbose));
fun print_theorems verbose =
@@ -400,7 +400,7 @@
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
let
val ctxt = Toplevel.context_of state;
- val {classes = (space, algebra), ...} = Type.rep_tsig (ProofContext.tsig_of ctxt);
+ val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
val classes = Sorts.classes_of algebra;
fun entry (c, (i, (_, cs))) =
(i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
@@ -421,7 +421,7 @@
let
val thy = Toplevel.theory_of state;
val ctxt = Toplevel.context_of state;
- fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
+ fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
val get_theory = Context.get_theory thy;
in
Thm_Deps.unused_thms
@@ -436,10 +436,10 @@
(* print proof context contents *)
val print_binds = Toplevel.unknown_context o
- Toplevel.keep (ProofContext.print_binds o Toplevel.context_of);
+ Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of);
val print_cases = Toplevel.unknown_context o
- Toplevel.keep (ProofContext.print_cases o Toplevel.context_of);
+ Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of);
(* print theorems, terms, types etc. *)
@@ -460,7 +460,7 @@
NONE =>
let
val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
--- a/src/Pure/Isar/local_defs.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML Sat Apr 16 15:47:52 2011 +0200
@@ -58,7 +58,7 @@
fun mk_def ctxt args =
let
val (xs, rhss) = split_list args;
- val (bind, _) = ProofContext.bind_fixes xs ctxt;
+ val (bind, _) = Proof_Context.bind_fixes xs ctxt;
val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
in map Logic.mk_equals (lhss ~~ rhss) end;
@@ -98,9 +98,9 @@
val lhss = map (fst o Logic.dest_equals) eqs;
in
ctxt
- |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+ |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
|> fold Variable.declare_term eqs
- |> ProofContext.add_assms_i def_export
+ |> Proof_Context.add_assms_i def_export
(map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
|>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
end;
@@ -117,7 +117,7 @@
val T = Term.fastype_of rhs;
val ([x'], ctxt') = ctxt
|> Variable.declare_term rhs
- |> ProofContext.add_fixes [(x, SOME T, mx)];
+ |> Proof_Context.add_fixes [(x, SOME T, mx)];
val lhs = Free (x', T);
val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
@@ -232,7 +232,7 @@
fun derived_def ctxt conditional prop =
let
val ((c, T), rhs) = prop
- |> Thm.cterm_of (ProofContext.theory_of ctxt)
+ |> Thm.cterm_of (Proof_Context.theory_of ctxt)
|> meta_rewrite_conv ctxt
|> (snd o Logic.dest_equals o Thm.prop_of)
|> conditional ? Logic.strip_imp_concl
--- a/src/Pure/Isar/local_theory.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/local_theory.ML Sat Apr 16 15:47:52 2011 +0200
@@ -134,10 +134,10 @@
fun raw_theory_result f lthy =
let
- val (res, thy') = f (ProofContext.theory_of lthy);
+ val (res, thy') = f (Proof_Context.theory_of lthy);
val lthy' = lthy
- |> map_target (ProofContext.transfer thy')
- |> ProofContext.transfer thy';
+ |> map_target (Proof_Context.transfer thy')
+ |> Proof_Context.transfer thy';
in (res, lthy') end;
fun raw_theory f = #2 o raw_theory_result (f #> pair ());
@@ -160,10 +160,10 @@
|> Context_Position.set_visible false
|> f
||> Context_Position.restore_visible lthy;
- val thy' = ProofContext.theory_of ctxt';
+ val thy' = Proof_Context.theory_of ctxt';
val lthy' = lthy
|> map_target (K ctxt')
- |> ProofContext.transfer thy';
+ |> Proof_Context.transfer thy';
in (res, lthy') end;
fun target f = #2 o target_result (f #> pair ());
@@ -181,12 +181,12 @@
(* morphisms *)
fun standard_morphism lthy ctxt =
- ProofContext.norm_export_morphism lthy ctxt $>
+ Proof_Context.norm_export_morphism lthy ctxt $>
Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
fun target_morphism lthy = standard_morphism lthy (target_of lthy);
fun global_morphism lthy =
- standard_morphism lthy (ProofContext.init_global (ProofContext.theory_of lthy));
+ standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
(* primitive operations *)
@@ -210,18 +210,18 @@
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
fun set_defsort S =
- syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (ProofContext.set_defsort S)));
+ syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
(* notation *)
fun type_notation add mode raw_args lthy =
let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
- in syntax_declaration false (ProofContext.target_type_notation add mode args) lthy end;
+ in syntax_declaration false (Proof_Context.target_type_notation add mode args) lthy end;
fun notation add mode raw_args lthy =
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
- in syntax_declaration false (ProofContext.target_notation add mode args) lthy end;
+ in syntax_declaration false (Proof_Context.target_notation add mode args) lthy end;
(* name space aliases *)
@@ -232,9 +232,9 @@
in Context.mapping (global_alias b' name) (local_alias b' name) end)
#> local_alias b name;
-val class_alias = alias Sign.class_alias ProofContext.class_alias;
-val type_alias = alias Sign.type_alias ProofContext.type_alias;
-val const_alias = alias Sign.const_alias ProofContext.const_alias;
+val class_alias = alias Sign.class_alias Proof_Context.class_alias;
+val type_alias = alias Sign.type_alias Proof_Context.type_alias;
+val const_alias = alias Sign.const_alias Proof_Context.const_alias;
@@ -244,7 +244,7 @@
fun init group theory_prefix operations target =
let val naming =
- Sign.naming_of (ProofContext.theory_of target)
+ Sign.naming_of (Proof_Context.theory_of target)
|> Name_Space.set_group group
|> Name_Space.mandatory_path theory_prefix;
in
@@ -261,8 +261,8 @@
(* exit *)
-val exit = ProofContext.background_theory Theory.checkpoint o operation #exit;
-val exit_global = ProofContext.theory_of o exit;
+val exit = Proof_Context.background_theory Theory.checkpoint o operation #exit;
+val exit_global = Proof_Context.theory_of o exit;
fun exit_result f (x, lthy) =
let
@@ -273,7 +273,7 @@
fun exit_result_global f (x, lthy) =
let
val thy = exit_global lthy;
- val thy_ctxt = ProofContext.init_global thy;
+ val thy_ctxt = Proof_Context.init_global thy;
val phi = standard_morphism lthy thy_ctxt;
in (f phi x, thy) end;
--- a/src/Pure/Isar/locale.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/locale.ML Sat Apr 16 15:47:52 2011 +0200
@@ -162,7 +162,7 @@
);
val intern = Name_Space.intern o #1 o Locales.get;
-fun extern thy = Name_Space.extern (ProofContext.init_global thy) (#1 (Locales.get thy));
+fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
val get_locale = Symtab.lookup o #2 o Locales.get;
val defined = Symtab.defined o #2 o Locales.get;
@@ -215,7 +215,7 @@
fun pretty_reg ctxt (name, morph) =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val name' = extern thy name;
fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
@@ -469,7 +469,7 @@
fun init name thy =
activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
- ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
+ ([], Context.Proof (Proof_Context.init_global thy)) |-> put_idents |> Context.proof_of;
(*** Add and extend registrations ***)
@@ -556,7 +556,7 @@
fun add_thmss loc kind args ctxt =
let
val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
- val ctxt'' = ctxt' |> ProofContext.background_theory
+ val ctxt'' = ctxt' |> Proof_Context.background_theory
((change_locale loc o apfst o apsnd) (cons (args', serial ()))
#>
(* Registrations *)
@@ -578,7 +578,7 @@
[([Drule.dummy_thm], [])])];
fun add_syntax_declaration loc decl =
- ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
+ Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
#> add_declaration loc decl;
@@ -631,7 +631,7 @@
fun print_locales thy =
Pretty.strs ("locales:" ::
- map #1 (Name_Space.extern_table (ProofContext.init_global thy) (Locales.get thy)))
+ map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
|> Pretty.writeln;
fun print_locale thy show_facts raw_name =
@@ -650,7 +650,7 @@
fun print_registrations ctxt raw_name =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val name = intern thy raw_name;
val _ = the_locale thy name; (* error if locale unknown *)
in
@@ -661,7 +661,7 @@
fun print_dependencies ctxt clean export insts =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val idents = if clean then [] else get_idents (Context.Proof ctxt);
in
(case fold (roundup thy cons export) insts (idents, []) |> snd of
--- a/src/Pure/Isar/method.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/method.ML Sat Apr 16 15:47:52 2011 +0200
@@ -154,7 +154,7 @@
fun cheating int ctxt =
if int orelse ! quick_and_dirty then
- METHOD (K (Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)))
+ METHOD (K (Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)))
else error "Cheating requires quick_and_dirty mode!";
@@ -183,8 +183,8 @@
(* fact -- composition by facts from context *)
-fun fact [] ctxt = SIMPLE_METHOD' (ProofContext.some_fact_tac ctxt)
- | fact rules _ = SIMPLE_METHOD' (ProofContext.fact_tac rules);
+fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
+ | fact rules _ = SIMPLE_METHOD' (Proof_Context.fact_tac rules);
(* assumption *)
@@ -334,7 +334,7 @@
fun print_methods thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
val meths = Methods.get thy;
fun prt_meth (name, (_, comment)) = Pretty.block
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
--- a/src/Pure/Isar/named_target.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/named_target.ML Sat Apr 16 15:47:52 2011 +0200
@@ -80,12 +80,12 @@
not is_canonical_class ?
(Context.mapping_result
(Sign.add_abbrev Print_Mode.internal arg)
- (ProofContext.add_abbrev Print_Mode.internal arg)
+ (Proof_Context.add_abbrev Print_Mode.internal arg)
#-> (fn (lhs' as Const (d, _), _) =>
same_shape ?
(Context.mapping
- (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
- Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
+ (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
+ Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
end;
fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
@@ -153,12 +153,12 @@
fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val target_name =
[Pretty.command (if is_class then "class" else "locale"),
Pretty.str (" " ^ Locale.extern thy target)];
val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
- (#1 (ProofContext.inferred_fixes ctxt));
+ (#1 (Proof_Context.inferred_fixes ctxt));
val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
(Assumption.all_assms_of ctxt);
val elems =
@@ -171,14 +171,14 @@
map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
in
Pretty.block [Pretty.command "theory", Pretty.brk 1,
- Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
+ Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
end;
(* init *)
fun init_context (Target {target, is_locale, is_class, ...}) =
- if not is_locale then ProofContext.init_global
+ if not is_locale then Proof_Context.init_global
else if not is_class then Locale.init target
else Class.init target;
--- a/src/Pure/Isar/object_logic.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/object_logic.ML Sat Apr 16 15:47:52 2011 +0200
@@ -188,7 +188,7 @@
fun atomize_prems ct =
if Logic.has_meta_prems (Thm.term_of ct) then
Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
- (ProofContext.init_global (Thm.theory_of_cterm ct)) ct
+ (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
else Conv.all_conv ct;
val atomize_prems_tac = CONVERSION atomize_prems;
--- a/src/Pure/Isar/obtain.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Sat Apr 16 15:47:52 2011 +0200
@@ -73,7 +73,7 @@
fun eliminate fix_ctxt rule xs As thm =
let
- val thy = ProofContext.theory_of fix_ctxt;
+ val thy = Proof_Context.theory_of fix_ctxt;
val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
@@ -99,8 +99,8 @@
fun bind_judgment ctxt name =
let
- val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
- val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
+ val (bind, ctxt') = Proof_Context.bind_fixes [name] ctxt;
+ val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name);
in ((v, t), ctxt') end;
val thatN = "that";
@@ -118,7 +118,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
- val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
+ val (_, fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
val xs = map (Variable.name o #1) vars;
(*obtain asms*)
@@ -134,7 +134,7 @@
val asm_frees = fold Term.add_frees asm_props [];
val parms = xs |> map (fn x =>
- let val x' = ProofContext.get_skolem fix_ctxt x
+ let val x' = Proof_Context.get_skolem fix_ctxt x
in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
val that_name = if name = "" then thatN else name;
@@ -166,8 +166,8 @@
in
-val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
-val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
+val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute Proof_Context.read_vars Proof_Context.read_propp;
end;
@@ -186,7 +186,7 @@
fun result tac facts ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val cert = Thm.cterm_of thy;
val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
@@ -212,7 +212,7 @@
fun unify_params vars thesis_var raw_rule ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
@@ -258,7 +258,7 @@
fun inferred_type (binding, _, mx) ctxt =
let
val x = Variable.name binding;
- val (T, ctxt') = ProofContext.inferred_param x ctxt
+ val (T, ctxt') = Proof_Context.inferred_param x ctxt
in ((x, T, mx), ctxt') end;
fun polymorphic ctxt vars =
@@ -280,7 +280,7 @@
let
val ((parms, rule), ctxt') =
unify_params vars thesis_var raw_rule (Proof.context_of state');
- val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt';
+ val (bind, _) = Proof_Context.bind_fixes (map (#1 o #1) parms) ctxt';
val ts = map (bind o Free o #1) parms;
val ps = map dest_Free ts;
val asms =
@@ -316,8 +316,8 @@
in
-val guess = gen_guess ProofContext.cert_vars;
-val guess_cmd = gen_guess ProofContext.read_vars;
+val guess = gen_guess Proof_Context.cert_vars;
+val guess_cmd = gen_guess Proof_Context.read_vars;
end;
--- a/src/Pure/Isar/overloading.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/overloading.ML Sat Apr 16 15:47:52 2011 +0200
@@ -65,8 +65,8 @@
let
val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
ImprovableSyntax.get ctxt;
- val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
- val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt;
+ val tsig = (Sign.tsig_of o Proof_Context.theory_of) ctxt;
+ val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
val passed_or_abbrev = passed orelse is_abbrev;
fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
of SOME ty_ty' => Type.typ_match tsig ty_ty'
@@ -85,7 +85,7 @@
if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
if passed_or_abbrev then SOME (ts'', ctxt)
else SOME (ts'', ctxt
- |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
+ |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
|> mark_passed)
end;
@@ -96,7 +96,7 @@
fun improve_term_uncheck ts ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
val ts' = map (rewrite_liberal thy unchecks) ts;
in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
@@ -104,7 +104,7 @@
fun set_primary_constraints ctxt =
let
val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
- in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
+ in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
val activate_improvable_syntax =
Context.proof_map
@@ -161,7 +161,7 @@
val overloading = get_overloading lthy;
fun pr_operation ((c, ty), (v, _)) =
Pretty.block (Pretty.breaks
- [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
+ [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
Pretty.str "::", Syntax.pretty_typ lthy ty]);
in Pretty.str "overloading" :: map pr_operation overloading end;
@@ -177,14 +177,14 @@
fun gen_overloading prep_const raw_overloading thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
val _ = if null raw_overloading then error "At least one parameter must be given" else ();
val overloading = raw_overloading |> map (fn (v, const, checked) =>
(Term.dest_Const (prep_const ctxt const), (v, checked)));
in
thy
|> Theory.checkpoint
- |> ProofContext.init_global
+ |> Proof_Context.init_global
|> Data.put overloading
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
|> activate_improvable_syntax
--- a/src/Pure/Isar/proof.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/proof.ML Sat Apr 16 15:47:52 2011 +0200
@@ -166,8 +166,8 @@
make_node (f (context, facts, mode, goal));
val init_context =
- ProofContext.set_stmt true #>
- ProofContext.map_naming (K ProofContext.local_naming);
+ Proof_Context.set_stmt true #>
+ Proof_Context.map_naming (K Proof_Context.local_naming);
fun init ctxt =
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
@@ -200,7 +200,7 @@
(* context *)
val context_of = #context o current;
-val theory_of = ProofContext.theory_of o context_of;
+val theory_of = Proof_Context.theory_of o context_of;
fun map_context f =
map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
@@ -213,8 +213,8 @@
fun propagate_ml_env state = map_contexts
(Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
-val bind_terms = map_context o ProofContext.bind_terms;
-val put_thms = map_context oo ProofContext.put_thms;
+val bind_terms = map_context o Proof_Context.bind_terms;
+val put_thms = map_context oo Proof_Context.put_thms;
(* facts *)
@@ -241,7 +241,7 @@
NONE => put_facts NONE outer
| SOME thms =>
thms
- |> ProofContext.export (context_of inner) (context_of outer)
+ |> Proof_Context.export (context_of inner) (context_of outer)
|> (fn ths => put_facts (SOME ths) outer));
@@ -324,7 +324,7 @@
(** pretty_state **)
-val verbose = ProofContext.verbose;
+val verbose = Proof_Context.verbose;
fun pretty_facts _ _ NONE = []
| pretty_facts s ctxt (SOME ths) =
@@ -357,8 +357,8 @@
| prt_goal NONE = [];
val prt_ctxt =
- if ! verbose orelse mode = Forward then ProofContext.pretty_context ctxt
- else if mode = Backward then ProofContext.pretty_ctxt ctxt
+ if ! verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
+ else if mode = Backward then Proof_Context.pretty_ctxt ctxt
else [];
in
[Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
@@ -404,8 +404,8 @@
Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
state
|> map_goal
- (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
- ProofContext.add_cases true meth_cases)
+ (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #>
+ Proof_Context.add_cases true meth_cases)
(K (statement, [], using, goal', before_qed, after_qed)))
end;
@@ -465,7 +465,7 @@
fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
in
raw_rules
- |> ProofContext.goal_export inner outer
+ |> Proof_Context.goal_export inner outer
|> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
end;
@@ -474,7 +474,7 @@
fun conclude_goal ctxt goal propss =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val string_of_term = Syntax.string_of_term ctxt;
val string_of_thm = Display.string_of_thm ctxt;
@@ -545,8 +545,8 @@
in
-val let_bind = gen_bind ProofContext.match_bind_i;
-val let_bind_cmd = gen_bind ProofContext.match_bind;
+val let_bind = gen_bind Proof_Context.match_bind_i;
+val let_bind_cmd = gen_bind Proof_Context.match_bind;
end;
@@ -557,7 +557,7 @@
fun gen_write prep_arg mode args =
assert_forward
- #> map_context (fn ctxt => ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args))
+ #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
#> put_facts NONE;
in
@@ -566,7 +566,7 @@
val write_cmd =
gen_write (fn ctxt => fn (c, mx) =>
- (ProofContext.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
+ (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
end;
@@ -577,13 +577,13 @@
fun gen_fix prep_vars args =
assert_forward
- #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
+ #> map_context (fn ctxt => snd (Proof_Context.add_fixes (prep_vars ctxt args) ctxt))
#> put_facts NONE;
in
val fix = gen_fix (K I);
-val fix_cmd = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
+val fix_cmd = gen_fix (fn ctxt => fn args => fst (Proof_Context.read_vars args ctxt));
end;
@@ -600,8 +600,8 @@
in
-val assm = gen_assume ProofContext.add_assms_i (K I);
-val assm_cmd = gen_assume ProofContext.add_assms Attrib.attribute;
+val assm = gen_assume Proof_Context.add_assms_i (K I);
+val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute;
val assume = assm Assumption.assume_export;
val assume_cmd = assm_cmd Assumption.assume_export;
val presume = assm Assumption.presume_export;
@@ -633,8 +633,8 @@
in
-val def = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
-val def_cmd = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
+val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
+val def_cmd = gen_def Attrib.attribute Proof_Context.read_vars Proof_Context.match_bind;
end;
@@ -666,7 +666,7 @@
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
state
|> assert_forward
- |> map_context_result (ProofContext.note_thmss ""
+ |> map_context_result (Proof_Context.note_thmss ""
(Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
|> these_factss (more_facts state)
||> opt_chain
@@ -675,13 +675,13 @@
in
val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
-val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
+val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute Proof_Context.get_fact;
val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
-val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
-val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
@@ -696,7 +696,7 @@
state
|> assert_backward
|> map_context_result
- (ProofContext.note_thmss ""
+ (Proof_Context.note_thmss ""
(Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
(no_binding args)))
|> (fn (named_facts, state') =>
@@ -713,9 +713,9 @@
in
val using = gen_using append_using (K (K I)) (K I) (K I);
-val using_cmd = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val using_cmd = gen_using append_using (K (K I)) Attrib.attribute Proof_Context.get_fact;
val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
-val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
+val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute Proof_Context.get_fact;
end;
@@ -731,7 +731,7 @@
let
val atts = map (prep_att (theory_of state)) raw_atts;
val (asms, state') = state |> map_context_result (fn ctxt =>
- ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
+ ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
in
state'
@@ -881,7 +881,7 @@
goal_state
|> map_context (init_context #> Variable.set_body true)
|> put_goal (SOME (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')))
- |> map_context (ProofContext.auto_bind_goal props)
+ |> map_context (Proof_Context.auto_bind_goal props)
|> chaining ? (`the_facts #-> using_facts)
|> put_facts NONE
|> open_block
@@ -902,7 +902,7 @@
|> Variable.exportT_terms goal_ctxt outer_ctxt;
val results =
tl (conclude_goal goal_ctxt goal stmt)
- |> burrow (ProofContext.export goal_ctxt outer_ctxt);
+ |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
in
outer_state
|> map_context (after_ctxt props)
@@ -932,7 +932,7 @@
fun local_qeds txt =
end_proof false txt
- #> Seq.map (generic_qed ProofContext.auto_bind_facts #->
+ #> Seq.map (generic_qed Proof_Context.auto_bind_facts #->
(fn ((after_qed, _), results) => after_qed results));
fun local_qed txt = local_qeds txt #> check_finish;
@@ -942,10 +942,10 @@
fun global_goal prepp before_qed after_qed propp ctxt =
init ctxt
- |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
+ |> generic_goal (prepp #> Proof_Context.auto_fixes) "" before_qed (K I, after_qed) propp;
-val theorem = global_goal ProofContext.bind_propp_schematic_i;
-val theorem_cmd = global_goal ProofContext.bind_propp_schematic;
+val theorem = global_goal Proof_Context.bind_propp_schematic_i;
+val theorem_cmd = global_goal Proof_Context.bind_propp_schematic;
fun global_qeds txt =
end_proof true txt
@@ -1017,10 +1017,10 @@
in
-val have = gen_have (K I) ProofContext.bind_propp_i;
-val have_cmd = gen_have Attrib.attribute ProofContext.bind_propp;
-val show = gen_show (K I) ProofContext.bind_propp_i;
-val show_cmd = gen_show Attrib.attribute ProofContext.bind_propp;
+val have = gen_have (K I) Proof_Context.bind_propp_i;
+val have_cmd = gen_have Attrib.attribute Proof_Context.bind_propp;
+val show = gen_show (K I) Proof_Context.bind_propp_i;
+val show_cmd = gen_show Attrib.attribute Proof_Context.bind_propp;
end;
@@ -1064,9 +1064,9 @@
(Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
fun after_local' [[th]] = put_thms false (Auto_Bind.thisN, SOME [th]);
- fun after_global' [[th]] = ProofContext.put_thms false (Auto_Bind.thisN, SOME [th]);
+ fun after_global' [[th]] = Proof_Context.put_thms false (Auto_Bind.thisN, SOME [th]);
val after_qed' = (after_local', after_global');
- val this_name = ProofContext.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
+ val this_name = Proof_Context.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
val result_ctxt =
state
@@ -1075,7 +1075,7 @@
|> fork_proof;
val future_thm = result_ctxt |> Future.map (fn (_, x) =>
- ProofContext.get_fact_single (get_context x) (Facts.named this_name));
+ Proof_Context.get_fact_single (get_context x) (Facts.named this_name));
val finished_goal = Goal.future_result goal_ctxt future_thm prop';
val state' =
state
--- a/src/Pure/Isar/proof_context.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Sat Apr 16 15:47:52 2011 +0200
@@ -161,10 +161,10 @@
val pretty_context: Proof.context -> Pretty.T list
end;
-structure ProofContext: PROOF_CONTEXT =
+structure Proof_Context: PROOF_CONTEXT =
struct
-open ProofContext;
+open Proof_Context;
(** inner syntax mode **)
@@ -597,7 +597,7 @@
local
-val dummies = Config.bool (Config.declare "ProofContext.dummies" (K (Config.Bool false)));
+val dummies = Config.bool (Config.declare "Proof_Context.dummies" (K (Config.Bool false)));
fun check_dummies ctxt t =
if Config.get ctxt dummies then t
@@ -1345,5 +1345,5 @@
end;
-val show_abbrevs = ProofContext.show_abbrevs;
+val show_abbrevs = Proof_Context.show_abbrevs;
--- a/src/Pure/Isar/proof_display.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML Sat Apr 16 15:47:52 2011 +0200
@@ -27,8 +27,8 @@
(* toplevel pretty printing *)
fun pp_context ctxt =
- (if ! ProofContext.debug then
- Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
+ (if ! Proof_Context.debug then
+ Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
else Pretty.str "<context>");
fun pp_thm th =
@@ -48,7 +48,7 @@
fun pretty_theorems_diff verbose prev_thys thy =
let
- val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
+ val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
val facts = Global_Theory.facts_of thy;
val thmss =
Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
@@ -87,7 +87,7 @@
fun pretty_facts ctxt =
flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
- map (single o ProofContext.pretty_fact_aux ctxt false);
+ map (single o Proof_Context.pretty_fact_aux ctxt false);
in
@@ -98,7 +98,7 @@
else Pretty.writeln
(case facts of
[fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
- ProofContext.pretty_fact_aux ctxt false fact])
+ Proof_Context.pretty_fact_aux ctxt false fact])
| _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
@@ -118,7 +118,7 @@
in
fun pretty_consts ctxt pred cs =
- (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
+ (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
[] => pretty_vars ctxt "constants" cs
| ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
--- a/src/Pure/Isar/rule_insts.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sat Apr 16 15:47:52 2011 +0200
@@ -83,7 +83,7 @@
val ts = map2 parse Ts ss;
val ts' =
map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
- |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
+ |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
|> Variable.polymorphic ctxt;
val Ts' = map Term.fastype_of ts';
val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
@@ -91,7 +91,7 @@
fun read_insts ctxt mixed_insts (tvars, vars) =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val cert = Thm.cterm_of thy;
val certT = Thm.ctyp_of thy;
@@ -193,7 +193,7 @@
(* instantiation of rule or goal state *)
fun read_instantiate ctxt args thm =
- read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *)
+ read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic) (* FIXME !? *)
(map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
@@ -260,7 +260,7 @@
fun bires_inst_tac bires_flag ctxt insts thm =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
(* Separate type and term insts *)
fun has_type_var ((x, _), _) =
(case Symbol.explode x of "'" :: _ => true | _ => false);
@@ -279,7 +279,7 @@
val (param_names, ctxt') = ctxt
|> Variable.declare_thm thm
|> Thm.fold_terms Variable.declare_constraints st
- |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+ |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
(* Process type insts: Tinsts_env *)
fun absent xi = error
--- a/src/Pure/Isar/skip_proof.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/skip_proof.ML Sat Apr 16 15:47:52 2011 +0200
@@ -35,10 +35,10 @@
(if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
(fn args => fn st =>
if ! quick_and_dirty
- then cheat_tac (ProofContext.theory_of ctxt) st
+ then cheat_tac (Proof_Context.theory_of ctxt) st
else tac args st);
fun prove_global thy xs asms prop tac =
- Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
+ Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
end;
--- a/src/Pure/Isar/spec_rules.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/spec_rules.ML Sat Apr 16 15:47:52 2011 +0200
@@ -48,7 +48,7 @@
fun add class (ts, ths) lthy =
let
- val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts;
+ val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
in
lthy |> Local_Theory.declaration true
(fn phi =>
--- a/src/Pure/Isar/specification.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/specification.ML Sat Apr 16 15:47:52 2011 +0200
@@ -117,10 +117,10 @@
fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
- val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
+ val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
val Asss =
(map o map) snd raw_specss
@@ -137,7 +137,7 @@
|> flat |> burrow (Syntax.check_props params_ctxt);
val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
- val Ts = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
+ val Ts = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
in ((params, name_atts ~~ specs), specs_ctxt) end;
@@ -152,17 +152,17 @@
in
-fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;
-fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true x;
+fun check_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) true x;
+fun read_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true x;
-fun check_free_spec x = prep_spec ProofContext.cert_vars (K I) (K I) false x;
-fun read_free_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src false x;
+fun check_free_spec x = prep_spec Proof_Context.cert_vars (K I) (K I) false x;
+fun read_free_spec x = prep_spec Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src false x;
fun check_specification vars specs =
- prepare ProofContext.cert_vars (K I) (K I) true vars [specs];
+ prepare Proof_Context.cert_vars (K I) (K I) true vars [specs];
fun read_specification vars specs =
- prepare ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
+ prepare Proof_Context.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
end;
@@ -171,7 +171,7 @@
fun gen_axioms do_print prep raw_vars raw_specs thy =
let
- val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init_global thy);
+ val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars;
(*consts*)
@@ -246,7 +246,7 @@
let
val ((vars, [(_, prop)]), _) =
prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
- (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
+ (lthy |> Proof_Context.set_mode Proof_Context.mode_abbrev);
val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
val var =
(case vars of
@@ -259,9 +259,9 @@
Position.str_of (Binding.pos_of b));
in (b, mx) end);
val lthy' = lthy
- |> ProofContext.set_syntax_mode mode (* FIXME ?!? *)
+ |> Proof_Context.set_syntax_mode mode (* FIXME ?!? *)
|> Local_Theory.abbrev mode (var, rhs) |> snd
- |> ProofContext.restore_syntax_mode lthy;
+ |> Proof_Context.restore_syntax_mode lthy;
val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
in lthy' end;
@@ -283,10 +283,10 @@
in
val type_notation = gen_type_notation (K I);
-val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
+val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false);
val notation = gen_notation (K I);
-val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false dummyT);
+val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);
end;
@@ -295,7 +295,7 @@
fun gen_theorems prep_fact prep_att kind raw_facts lthy =
let
- val attrib = prep_att (ProofContext.theory_of lthy);
+ val attrib = prep_att (Proof_Context.theory_of lthy);
val facts = raw_facts |> map (fn ((name, atts), bs) =>
((name, map attrib atts),
bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
@@ -304,7 +304,7 @@
in (res, lthy') end;
val theorems = gen_theorems (K I) (K I);
-val theorems_cmd = gen_theorems ProofContext.get_fact Attrib.intern_src;
+val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.intern_src;
(* complex goal statements *)
@@ -331,7 +331,7 @@
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
- val thesis = Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
+ val thesis = Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) Auto_Bind.thesisN;
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
@@ -340,12 +340,12 @@
val props = map fst asms;
val (Ts, _) = ctxt'
|> fold Variable.declare_term props
- |> fold_map ProofContext.inferred_param xs;
+ |> fold_map Proof_Context.inferred_param xs;
val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
in
- ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
+ ctxt' |> (snd o Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
ctxt' |> Variable.auto_fixes asm
- |> ProofContext.add_assms_i Assumption.assume_export
+ |> Proof_Context.add_assms_i Assumption.assume_export
[((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
|>> (fn [(_, [th])] => th)
end;
@@ -356,10 +356,10 @@
val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
- |> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
+ |> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
|-> (fn ths =>
- ProofContext.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
+ Proof_Context.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
#2 #> pair ths);
in ((prems, stmt, SOME facts), goal_ctxt) end);
@@ -375,7 +375,7 @@
kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
let
val _ = Local_Theory.affirm lthy;
- val thy = ProofContext.theory_of lthy;
+ val thy = Proof_Context.theory_of lthy;
val attrib = prep_att thy;
val atts = map attrib raw_atts;
@@ -385,7 +385,7 @@
fun after_qed' results goal_ctxt' =
let val results' =
- burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
+ burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results
in
lthy
|> Local_Theory.notes_kind kind
@@ -403,7 +403,7 @@
end;
in
goal_ctxt
- |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
+ |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
--- a/src/Pure/Isar/toplevel.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Apr 16 15:47:52 2011 +0200
@@ -516,7 +516,7 @@
fun theory_to_proof f = begin_proof
(K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
- (K (Context.Theory o Sign.reset_group o ProofContext.theory_of));
+ (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
end;
@@ -660,7 +660,7 @@
else
let
val (body_trs, end_tr) = split_last proof_trs;
- val finish = Context.Theory o ProofContext.theory_of;
+ val finish = Context.Theory o Proof_Context.theory_of;
val future_proof = Proof.global_future_proof
(fn prf =>
--- a/src/Pure/Isar/typedecl.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/typedecl.ML Sat Apr 16 15:47:52 2011 +0200
@@ -51,7 +51,7 @@
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
- val args = map (TFree o ProofContext.check_tfree lthy) raw_args;
+ val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
val T = Type (Local_Theory.full_name lthy b, args);
val bad_args =
@@ -98,7 +98,7 @@
fun read_abbrev b ctxt raw_rhs =
let
- val rhs = ProofContext.read_typ_syntax (ctxt |> ProofContext.set_defsort []) raw_rhs;
+ val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs;
val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
val _ =
if null ignored then ()
@@ -110,7 +110,7 @@
in
-val abbrev = gen_abbrev (K ProofContext.cert_typ_syntax);
+val abbrev = gen_abbrev (K Proof_Context.cert_typ_syntax);
val abbrev_cmd = gen_abbrev read_abbrev;
end;
--- a/src/Pure/ML/ml_antiquote.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Sat Apr 16 15:47:52 2011 +0200
@@ -80,12 +80,12 @@
val _ = macro "let" (Args.context --
Scan.lift
(Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
- >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
+ >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt)));
val _ = macro "note" (Args.context :|-- (fn ctxt =>
Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
- ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
- >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
+ ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
+ >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt))));
val _ = value "ctyp" (Args.typ >> (fn T =>
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
@@ -97,14 +97,14 @@
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
val _ = value "cpat"
- (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
+ (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
(* type classes *)
fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
- ProofContext.read_class ctxt s
+ Proof_Context.read_class ctxt s
|> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
@@ -120,8 +120,8 @@
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
>> (fn (ctxt, (s, pos)) =>
let
- val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
- val decl = Type.the_decl (ProofContext.tsig_of ctxt) c;
+ val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
+ val decl = Type.the_decl (Proof_Context.tsig_of ctxt) c;
val res =
(case try check (c, decl) of
SOME res => res
@@ -139,8 +139,8 @@
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
>> (fn (ctxt, (s, pos)) =>
let
- val Const (c, _) = ProofContext.read_const_proper ctxt false s;
- val res = check (ProofContext.consts_of ctxt, c)
+ val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
+ val res = check (Proof_Context.consts_of ctxt, c)
handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
in ML_Syntax.print_string res end);
@@ -151,7 +151,7 @@
val _ = inline "syntax_const"
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
- if is_some (Syntax.lookup_const (ProofContext.syn_of ctxt) c)
+ if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
then ML_Syntax.print_string c
else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
@@ -160,8 +160,8 @@
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, raw_c), Ts) =>
let
- val Const (c, _) = ProofContext.read_const_proper ctxt true raw_c;
- val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts));
+ val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
+ val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
in ML_Syntax.atomic (ML_Syntax.print_term const) end));
end;
--- a/src/Pure/ML/ml_context.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/ML/ml_context.ML Sat Apr 16 15:47:52 2011 +0200
@@ -48,8 +48,8 @@
val the_global_context = Context.theory_of o the_generic_context;
val the_local_context = Context.proof_of o the_generic_context;
-fun thm name = ProofContext.get_thm (the_local_context ()) name;
-fun thms name = ProofContext.get_thms (the_local_context ()) name;
+fun thm name = Proof_Context.get_thm (the_local_context ()) name;
+fun thms name = Proof_Context.get_thms (the_local_context ()) name;
fun exec (e: unit -> unit) context =
(case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
--- a/src/Pure/ML/ml_thms.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/ML/ml_thms.ML Sat Apr 16 15:47:52 2011 +0200
@@ -62,7 +62,7 @@
val i = serial ();
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
fun after_qed res goal_ctxt =
- put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
+ put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
val ctxt' = ctxt
|> Proof.theorem NONE after_qed propss
|> Proof.global_terminal_proof methods;
--- a/src/Pure/Proof/extraction.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Proof/extraction.ML Sat Apr 16 15:47:52 2011 +0200
@@ -162,9 +162,9 @@
fun read_term thy T s =
let
- val ctxt = ProofContext.init_global thy
+ val ctxt = Proof_Context.init_global thy
|> Proof_Syntax.strip_sorts_consttypes
- |> ProofContext.set_defsort [];
+ |> Proof_Context.set_defsort [];
val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
--- a/src/Pure/Proof/proof_syntax.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sat Apr 16 15:47:52 2011 +0200
@@ -202,9 +202,9 @@
end;
fun strip_sorts_consttypes ctxt =
- let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt)
+ let val {constants = (_, tab), ...} = Consts.dest (Proof_Context.consts_of ctxt)
in Symtab.fold (fn (s, (T, _)) =>
- ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T)))
+ Proof_Context.add_const_constraint (s, SOME (Type.strip_sorts T)))
tab ctxt
end;
@@ -216,12 +216,12 @@
|> add_proof_syntax
|> add_proof_atom_consts
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
- |> ProofContext.init_global
- |> ProofContext.allow_dummies
- |> ProofContext.set_mode ProofContext.mode_schematic
+ |> Proof_Context.init_global
+ |> Proof_Context.allow_dummies
+ |> Proof_Context.set_mode Proof_Context.mode_schematic
|> (if topsort then
strip_sorts_consttypes #>
- ProofContext.set_defsort []
+ Proof_Context.set_defsort []
else I);
in
fn ty => fn s =>
@@ -259,8 +259,8 @@
in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
fun pretty_proof ctxt prf =
- ProofContext.pretty_term_abbrev
- (ProofContext.transfer_syntax (proof_syntax prf (ProofContext.theory_of ctxt)) ctxt)
+ Proof_Context.pretty_term_abbrev
+ (Proof_Context.transfer_syntax (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
(term_of_proof prf);
fun pretty_proof_of ctxt full th =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Apr 16 15:47:52 2011 +0200
@@ -522,7 +522,7 @@
fun thms_of_thy name =
let val thy = Thy_Info.get_theory name
- in map fst (theory_facts thy |-> Facts.extern_static (ProofContext.init_global thy)) end;
+ in map fst (theory_facts thy |-> Facts.extern_static (Proof_Context.init_global thy)) end;
fun qualified_thms_of_thy name =
map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static);
@@ -610,7 +610,7 @@
(* TODO: interim: this is probably not right.
What we want is mapping onto simple PGIP name/context model. *)
val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
- val thy = ProofContext.theory_of ctx
+ val thy = Proof_Context.theory_of ctx
val ths = [Global_Theory.get_thm thy thmname]
val deps = #2 (thms_deps ths);
in
--- a/src/Pure/Syntax/syntax.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Sat Apr 16 15:47:52 2011 +0200
@@ -344,10 +344,10 @@
val read_term = singleton o read_terms;
val read_prop = singleton o read_props;
-val read_sort_global = read_sort o ProofContext.init_global;
-val read_typ_global = read_typ o ProofContext.init_global;
-val read_term_global = read_term o ProofContext.init_global;
-val read_prop_global = read_prop o ProofContext.init_global;
+val read_sort_global = read_sort o Proof_Context.init_global;
+val read_typ_global = read_typ o Proof_Context.init_global;
+val read_term_global = read_term o Proof_Context.init_global;
+val read_prop_global = read_prop o Proof_Context.init_global;
(* pretty = uncheck + unparse *)
@@ -370,7 +370,7 @@
val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
fun is_pretty_global ctxt = Config.get ctxt pretty_global;
val set_pretty_global = Config.put pretty_global;
-val init_pretty_global = set_pretty_global true o ProofContext.init_global;
+val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
val pretty_term_global = pretty_term o init_pretty_global;
val pretty_typ_global = pretty_typ o init_pretty_global;
--- a/src/Pure/Syntax/syntax_phases.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Apr 16 15:47:52 2011 +0200
@@ -21,13 +21,13 @@
(** markup logical entities **)
fun markup_class ctxt c =
- [Name_Space.markup_entry (Type.class_space (ProofContext.tsig_of ctxt)) c];
+ [Name_Space.markup_entry (Type.class_space (Proof_Context.tsig_of ctxt)) c];
fun markup_type ctxt c =
- [Name_Space.markup_entry (Type.type_space (ProofContext.tsig_of ctxt)) c];
+ [Name_Space.markup_entry (Type.type_space (Proof_Context.tsig_of ctxt)) c];
fun markup_const ctxt c =
- [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c];
+ [Name_Space.markup_entry (Consts.space_of (Proof_Context.consts_of ctxt)) c];
fun markup_free ctxt x =
[if can Name.dest_skolem x then Markup.skolem else Markup.free] @
@@ -40,7 +40,7 @@
[Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
fun markup_entity ctxt c =
- (case Syntax.lookup_const (ProofContext.syn_of ctxt) c of
+ (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
SOME "" => []
| SOME b => markup_entity ctxt b
| NONE => c |> Lexicon.unmark
@@ -125,8 +125,8 @@
fun parsetree_to_ast ctxt constrain_pos trf parsetree =
let
- val get_class = ProofContext.read_class ctxt;
- val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
+ val get_class = Proof_Context.read_class ctxt;
+ val get_type = #1 o dest_Type o Proof_Context.read_type_name_proper ctxt false;
val reports = Unsynchronized.ref ([]: Position.reports);
fun report pos = Position.reports reports [pos];
@@ -197,11 +197,11 @@
| decode_term ctxt (reports0, Exn.Result tm) =
let
fun get_const a =
- ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
- handle ERROR _ => (false, Consts.intern (ProofContext.consts_of ctxt) a));
- val get_free = ProofContext.intern_skolem ctxt;
+ ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
+ handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
+ val get_free = Proof_Context.intern_skolem ctxt;
- val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
+ val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
val reports = Unsynchronized.ref reports0;
fun report ps = Position.reports reports ps;
@@ -272,7 +272,7 @@
fun parse_asts ctxt raw root (syms, pos) =
let
- val syn = ProofContext.syn_of ctxt;
+ val syn = Proof_Context.syn_of ctxt;
val ast_tr = Syntax.parse_ast_translation syn;
val toks = Syntax.tokenize syn raw syms;
@@ -301,7 +301,7 @@
fun parse_raw ctxt root input =
let
- val syn = ProofContext.syn_of ctxt;
+ val syn = Proof_Context.syn_of ctxt;
val tr = Syntax.parse_translation syn;
val parse_rules = Syntax.parse_rules syn;
in
@@ -325,7 +325,7 @@
|> report_result ctxt pos
|> sort_of_term
handle ERROR msg => parse_failed ctxt pos msg "sort";
- in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
+ in Type.minimize_sort (Proof_Context.tsig_of ctxt) S end;
fun parse_typ ctxt text =
let
@@ -333,7 +333,7 @@
val T =
parse_raw ctxt "type" (syms, pos)
|> report_result ctxt pos
- |> (fn t => typ_of_term (ProofContext.get_sort ctxt (term_sorts t)) t)
+ |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
handle ERROR msg => parse_failed ctxt pos msg "type";
in T end;
@@ -398,7 +398,7 @@
fun parse_ast_pattern ctxt (root, str) =
let
- val syn = ProofContext.syn_of ctxt;
+ val syn = Proof_Context.syn_of ctxt;
fun constify (ast as Ast.Constant _) = ast
| constify (ast as Ast.Variable x) =
@@ -590,7 +590,7 @@
else Markup.hilite;
in
if can Name.dest_skolem x
- then ([m, Markup.skolem], ProofContext.revert_skolem ctxt x)
+ then ([m, Markup.skolem], Proof_Context.revert_skolem ctxt x)
else ([m, Markup.free], x)
end;
@@ -604,7 +604,7 @@
fun unparse_t t_to_ast prt_t markup ctxt t =
let
- val syn = ProofContext.syn_of ctxt;
+ val syn = Proof_Context.syn_of ctxt;
fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
| token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
@@ -620,9 +620,9 @@
SOME "" => ([], c)
| SOME b => markup_extern b
| NONE => c |> Lexicon.unmark
- {case_class = fn x => ([Markup.tclass x], ProofContext.extern_class ctxt x),
- case_type = fn x => ([Markup.tycon x], ProofContext.extern_type ctxt x),
- case_const = fn x => ([Markup.const x], ProofContext.extern_const ctxt x),
+ {case_class = fn x => ([Markup.tclass x], Proof_Context.extern_class ctxt x),
+ case_type = fn x => ([Markup.tycon x], Proof_Context.extern_type ctxt x),
+ case_const = fn x => ([Markup.const x], Proof_Context.extern_const ctxt x),
case_fixed = fn x => free_or_skolem ctxt x,
case_default = fn x => ([], x)});
in
@@ -639,9 +639,9 @@
fun unparse_term ctxt =
let
- val thy = ProofContext.theory_of ctxt;
- val syn = ProofContext.syn_of ctxt;
- val idents = Local_Syntax.idents_of (ProofContext.syntax_of ctxt);
+ val thy = Proof_Context.theory_of ctxt;
+ val syn = Proof_Context.syn_of ctxt;
+ val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
in
unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
(Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
@@ -681,7 +681,7 @@
fun const_ast_tr intern ctxt [Ast.Variable c] =
let
- val Const (c', _) = ProofContext.read_const_proper ctxt false c;
+ val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
val d = if intern then Lexicon.mark_const c' else c;
in Ast.Constant d end
| const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T]] =
--- a/src/Pure/Thy/term_style.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Thy/term_style.ML Sat Apr 16 15:47:52 2011 +0200
@@ -45,7 +45,7 @@
fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse)
>> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
- (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
+ (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
(Args.src x) ctxt |>> (fn f => f ctxt)));
val parse = Args.context :|-- (fn ctxt => Scan.lift
@@ -56,7 +56,7 @@
val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style.";
Scan.lift Args.liberal_name
>> (fn name => fst (Args.context_syntax "style"
- (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
+ (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
(Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))));
@@ -65,7 +65,7 @@
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
let
val concl =
- Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+ Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
in
case concl of (_ $ l $ r) => proj (l, r)
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
--- a/src/Pure/Thy/thy_output.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat Apr 16 15:47:52 2011 +0200
@@ -491,35 +491,35 @@
fun pretty_const ctxt c =
let
- val t = Const (c, Consts.type_scheme (ProofContext.consts_of ctxt) c)
+ val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
handle TYPE (msg, _, _) => error msg;
val ([t'], _) = Variable.import_terms true [t] ctxt;
in pretty_term ctxt t' end;
fun pretty_abbrev ctxt s =
let
- val t = Syntax.parse_term ctxt s |> singleton (ProofContext.standard_infer_types ctxt);
+ val t = Syntax.parse_term ctxt s |> singleton (Proof_Context.standard_infer_types ctxt);
fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
val (head, args) = Term.strip_comb t;
val (c, T) = Term.dest_Const head handle TERM _ => err ();
- val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
+ val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
handle TYPE _ => err ();
val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
val eq = Logic.mk_equals (t, t');
val ctxt' = Variable.auto_fixes eq ctxt;
- in ProofContext.pretty_term_abbrev ctxt' eq end;
+ in Proof_Context.pretty_term_abbrev ctxt' eq end;
fun pretty_class ctxt =
- Pretty.str o ProofContext.extern_class ctxt o ProofContext.read_class ctxt;
+ Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
fun pretty_type ctxt s =
- let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
- in Pretty.str (ProofContext.extern_type ctxt name) end;
+ let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
+ in Pretty.str (Proof_Context.extern_type ctxt name) end;
fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
fun pretty_theory ctxt name =
- (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
+ (Theory.requires (Proof_Context.theory_of ctxt) name "presentation"; Pretty.str name);
(* default output *)
--- a/src/Pure/Tools/find_consts.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Tools/find_consts.ML Sat Apr 16 15:47:52 2011 +0200
@@ -71,7 +71,7 @@
let
val start = Timing.start ();
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val low_ranking = 10000;
fun user_visible consts (nm, _) =
@@ -82,7 +82,7 @@
val raw_T = Syntax.parse_typ ctxt crit;
val t =
Syntax.check_term
- (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+ (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
(Term.dummy_pattern raw_T);
in Term.type_of t end;
--- a/src/Pure/Tools/find_theorems.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML Sat Apr 16 15:47:52 2011 +0200
@@ -43,15 +43,15 @@
fun parse_pattern ctxt nm =
let
- val consts = ProofContext.consts_of ctxt;
+ val consts = Proof_Context.consts_of ctxt;
val nm' =
(case Syntax.parse_term ctxt nm of
Const (c, _) => c
| _ => Consts.intern consts nm);
in
(case try (Consts.the_abbreviation consts) nm' of
- SOME (_, rhs) => apply_dummies (ProofContext.expand_abbrevs ctxt rhs)
- | NONE => ProofContext.read_term_pattern ctxt nm)
+ SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs)
+ | NONE => Proof_Context.read_term_pattern ctxt nm)
end;
fun read_criterion _ (Name name) = Name name
@@ -60,7 +60,7 @@
| read_criterion _ Elim = Elim
| read_criterion _ Dest = Dest
| read_criterion _ Solves = Solves
- | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str)
+ | read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str)
| read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str);
fun pretty_criterion ctxt (b, c) =
@@ -131,7 +131,7 @@
returns: smallest substitution size*)
fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
fun matches pat =
@@ -216,7 +216,7 @@
in
(*elim rules always have assumptions, so an elim with one
assumption is as good as an intro rule with none*)
- if is_nontrivial (ProofContext.theory_of ctxt) (major_prem_of theorem)
+ if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem)
andalso not (null successful)
then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
end
@@ -274,7 +274,7 @@
fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem)))
| check (theorem, c as SOME thm_consts) =
(if subset (op =) (pat_consts, thm_consts) andalso
- Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, prop_of theorem)
+ Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem)
then SOME (0, 0) else NONE, c);
in check end;
@@ -378,7 +378,7 @@
fun nicer_shortest ctxt =
let
(* FIXME global name space!? *)
- val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
+ val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
val shorten =
Name_Space.extern
@@ -412,10 +412,10 @@
|> filter_out (Facts.is_concealed facts o #1);
in
maps Facts.selections
- (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
+ (visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @
- visible_facts (ProofContext.facts_of ctxt))
+ visible_facts (Proof_Context.facts_of ctxt))
end;
val limit = Unsynchronized.ref 40;
@@ -423,7 +423,7 @@
fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
let
val assms =
- ProofContext.get_fact ctxt (Facts.named "local.assms")
+ Proof_Context.get_fact ctxt (Facts.named "local.assms")
handle ERROR _ => [];
val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
val opt_goal' = Option.map add_prems opt_goal;
--- a/src/Pure/axclass.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/axclass.ML Sat Apr 16 15:47:52 2011 +0200
@@ -198,7 +198,7 @@
(case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
SOME thm => thm
| NONE => error ("Unproven class relation " ^
- Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2])); (* FIXME stale thy (!?) *)
+ Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2])); (* FIXME stale thy (!?) *)
fun put_trancl_classrel ((c1, c2), th) thy =
let
@@ -245,7 +245,7 @@
(case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
SOME (thm, _) => thm
| NONE => error ("Unproven type arity " ^
- Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c]))); (* FIXME stale thy (!?) *)
+ Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); (* FIXME stale thy (!?) *)
fun thynames_of_arity thy (c, a) =
Symtab.lookup_list (proven_arities_of thy) a
@@ -359,7 +359,7 @@
in (c1, c2) end;
fun read_classrel thy raw_rel =
- cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel)
+ cert_classrel thy (pairself (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel)
handle TYPE (msg, _, _) => error msg;
@@ -464,7 +464,7 @@
fun prove_classrel raw_rel tac thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
val (c1, c2) = cert_classrel thy raw_rel;
val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
@@ -475,8 +475,8 @@
fun prove_arity raw_arity tac thy =
let
- val ctxt = ProofContext.init_global thy;
- val arity = ProofContext.cert_arity ctxt raw_arity;
+ val ctxt = Proof_Context.init_global thy;
+ val arity = Proof_Context.cert_arity ctxt raw_arity;
val names = map (prefix arity_prefix) (Logic.name_arities arity);
val props = Logic.mk_arities arity;
val ths = Goal.prove_multi ctxt [] [] props
@@ -617,7 +617,7 @@
(map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
fun ax_arity prep =
- axiomatize (prep o ProofContext.init_global) Logic.mk_arities
+ axiomatize (prep o Proof_Context.init_global) Logic.mk_arities
(map (prefix arity_prefix) o Logic.name_arities) add_arity;
fun class_const c =
@@ -637,11 +637,11 @@
in
val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
+val axiomatize_class_cmd = ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
val axiomatize_classrel = ax_classrel cert_classrel;
val axiomatize_classrel_cmd = ax_classrel read_classrel;
-val axiomatize_arity = ax_arity ProofContext.cert_arity;
-val axiomatize_arity_cmd = ax_arity ProofContext.read_arity;
+val axiomatize_arity = ax_arity Proof_Context.cert_arity;
+val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity;
end;
--- a/src/Pure/codegen.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/codegen.ML Sat Apr 16 15:47:52 2011 +0200
@@ -821,7 +821,7 @@
val generate_code_i = gen_generate_code Sign.cert_term;
val generate_code =
- gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init_global);
+ gen_generate_code (Syntax.read_term o Proof_Context.allow_dummies o Proof_Context.init_global);
(**** Reflection ****)
@@ -872,7 +872,7 @@
fun test_term ctxt t =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
(generate_code_i thy [] "Generated") [("testf", t)];
val Ts = map snd (fst (strip_abs t));
@@ -906,7 +906,7 @@
fun eval_term thy t =
let
- val ctxt = ProofContext.init_global thy; (* FIXME *)
+ val ctxt = Proof_Context.init_global thy; (* FIXME *)
val e =
let
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
--- a/src/Pure/context.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/context.ML Sat Apr 16 15:47:52 2011 +0200
@@ -17,7 +17,7 @@
type theory_ref
exception THEORY of string * theory list
structure Proof: sig type context end
- structure ProofContext:
+ structure Proof_Context:
sig
val theory_of: Proof.context -> theory
val init_global: theory -> Proof.context
@@ -492,7 +492,7 @@
val thy_ref' = check_thy thy';
in Proof.Context (data', thy_ref') end;
-structure ProofContext =
+structure Proof_Context =
struct
val theory_of = theory_of_proof;
fun init_global thy = Proof.Context (init_data thy, check_thy thy);
@@ -510,7 +510,7 @@
fun get k dest prf =
dest (case Datatab.lookup (data_of_proof prf) k of
SOME x => x
- | NONE => invoke_init k (ProofContext.theory_of prf)); (*adhoc value*)
+ | NONE => invoke_init k (Proof_Context.theory_of prf)); (*adhoc value*)
fun put k mk x = map_prf (Datatab.update (k, mk x));
@@ -542,8 +542,8 @@
fun theory_map f = the_theory o f o Theory;
fun proof_map f = the_proof o f o Proof;
-val theory_of = cases I ProofContext.theory_of;
-val proof_of = cases ProofContext.init_global I;
+val theory_of = cases I Proof_Context.theory_of;
+val proof_of = cases Proof_Context.init_global I;
--- a/src/Pure/goal.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/goal.ML Sat Apr 16 15:47:52 2011 +0200
@@ -154,7 +154,7 @@
fun future_result ctxt result prop =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val _ = Context.reject_draft thy;
val cert = Thm.cterm_of thy;
val certT = Thm.ctyp_of thy;
@@ -203,7 +203,7 @@
fun prove_common immediate ctxt xs asms props tac =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val string_of_term = Syntax.string_of_term ctxt;
val pos = Position.thread_data ();
@@ -252,7 +252,7 @@
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
fun prove_global thy xs asms prop tac =
- Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
+ Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
--- a/src/Pure/pure_setup.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/pure_setup.ML Sat Apr 16 15:47:52 2011 +0200
@@ -56,3 +56,7 @@
val cd = File.cd o Path.explode;
Proofterm.proofs := 0;
+
+(*legacy*)
+structure ProofContext = Proof_Context;
+
--- a/src/Pure/raw_simplifier.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Sat Apr 16 15:47:52 2011 +0200
@@ -316,7 +316,7 @@
in
fun print_term_global ss warn a thy t =
- print_term ss warn (K a) t (ProofContext.init_global thy);
+ print_term ss warn (K a) t (Proof_Context.init_global thy);
fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
@@ -365,13 +365,13 @@
fun context ctxt =
map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
-val global_context = context o ProofContext.init_global;
+val global_context = context o Proof_Context.init_global;
fun activate_context thy ss =
let
val ctxt = the_context ss;
val ctxt' = ctxt
- |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
+ |> Context.raw_transfer (Theory.merge (thy, Proof_Context.theory_of ctxt))
|> Context_Position.set_visible false;
in context ctxt' ss end;
@@ -639,7 +639,7 @@
fun mk_simproc name lhss proc =
make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
- proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
+ proc (Proof_Context.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
(* FIXME avoid global thy and Logic.varify_global *)
fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
--- a/src/Pure/sign.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/sign.ML Sat Apr 16 15:47:52 2011 +0200
@@ -350,7 +350,7 @@
fun gen_syntax change_gram parse_typ mode args thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
@@ -387,7 +387,7 @@
fun gen_add_consts parse_typ raw_args thy =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
fun prep (b, raw_T, mx) =
let
--- a/src/Pure/simplifier.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/simplifier.ML Sat Apr 16 15:47:52 2011 +0200
@@ -132,7 +132,7 @@
fun map_simpset f = Context.theory_map (map_ss f);
fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
fun global_simpset_of thy =
- Raw_Simplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
+ Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
@@ -193,7 +193,7 @@
|> fold Variable.declare_term lhss'
|> fold Variable.auto_fixes lhss';
in Variable.export_terms ctxt' lthy lhss' end
- |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
+ |> map (Thm.cterm_of (Proof_Context.theory_of lthy)),
proc = proc,
identifier = identifier};
in
--- a/src/Pure/subgoal.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/subgoal.ML Sat Apr 16 15:47:52 2011 +0200
@@ -67,7 +67,7 @@
*)
fun lift_import idx params th ctxt =
let
- val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
+ val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
val Ts = map (#T o Thm.rep_cterm) params;
--- a/src/Pure/theory.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/theory.ML Sat Apr 16 15:47:52 2011 +0200
@@ -240,7 +240,7 @@
fun check_def thy unchecked overloaded (b, tm) defs =
let
- val ctxt = ProofContext.init_global thy;
+ val ctxt = Proof_Context.init_global thy;
val name = Sign.full_name thy b;
val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
handle TERM (msg, _) => error msg;
--- a/src/Pure/thm.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/thm.ML Sat Apr 16 15:47:52 2011 +0200
@@ -1735,7 +1735,7 @@
);
fun extern_oracles ctxt =
- map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt)));
+ map #1 (Name_Space.extern_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
fun add_oracle (b, oracle) thy =
let
--- a/src/Pure/type_infer.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/type_infer.ML Sat Apr 16 15:47:52 2011 +0200
@@ -219,7 +219,7 @@
fun unify ctxt pp =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
--- a/src/Pure/variable.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/variable.ML Sat Apr 16 15:47:52 2011 +0200
@@ -239,7 +239,7 @@
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
val declare_thm = Thm.fold_terms declare_internal;
-fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th));
+fun global_thm_context th = declare_thm th (Proof_Context.init_global (Thm.theory_of_thm th));
(* renaming term/type frees *)
@@ -430,7 +430,7 @@
fun importT ths ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
val ths' = map (Thm.instantiate insts') ths;
@@ -444,7 +444,7 @@
fun import is_open ths ctxt =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
val insts' = Thm.certify_inst thy insts;
val ths' = map (Thm.instantiate insts') ths;