# HG changeset patch # User wenzelm # Date 1302961672 -7200 # Node ID da8817d01e7c3c65902135e202493bb0bce7a592 # Parent 6ca5407863ed1df277431154becaa6eab3ec1321 modernized structure Proof_Context; diff -r 6ca5407863ed -r da8817d01e7c NEWS --- 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. diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/args.ML --- 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 | _ => ""); diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/attrib.ML --- 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 #> diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/calculation.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/class.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/class_declaration.ML --- 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*) diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/code.ML --- 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 = diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/element.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/expression.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/generic_target.ML --- 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) = diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/isar_cmd.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/local_defs.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/local_theory.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/locale.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/method.ML --- 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]; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/named_target.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/object_logic.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/obtain.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/overloading.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/proof.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/proof_context.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/proof_display.ML --- 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 ""); 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]); diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/rule_insts.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/skip_proof.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/spec_rules.ML --- 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 => diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/specification.ML --- 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) diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/toplevel.ML --- 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 => diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Isar/typedecl.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/ML/ml_antiquote.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/ML/ml_context.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/ML/ml_thms.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Proof/extraction.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Proof/proof_syntax.ML --- 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 = diff -r 6ca5407863ed -r da8817d01e7c src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Syntax/syntax.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Syntax/syntax_phases.ML --- 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]] = diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Thy/term_style.ML --- 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) diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Thy/thy_output.ML --- 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 *) diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Tools/find_consts.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/Tools/find_theorems.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/axclass.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/codegen.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/context.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/goal.ML --- 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); diff -r 6ca5407863ed -r da8817d01e7c src/Pure/pure_setup.ML --- 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; + diff -r 6ca5407863ed -r da8817d01e7c src/Pure/raw_simplifier.ML --- 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); diff -r 6ca5407863ed -r da8817d01e7c src/Pure/sign.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/simplifier.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/subgoal.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/theory.ML --- 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; diff -r 6ca5407863ed -r da8817d01e7c src/Pure/thm.ML --- 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 diff -r 6ca5407863ed -r da8817d01e7c src/Pure/type_infer.ML --- 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); diff -r 6ca5407863ed -r da8817d01e7c src/Pure/variable.ML --- 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;