--- a/src/HOL/Library/OptionalSugar.thy Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Library/OptionalSugar.thy Mon Nov 02 13:43:50 2009 -0800
@@ -50,7 +50,7 @@
(* type constraints with spacing *)
setup {*
let
- val typ = SimpleSyntax.read_typ;
+ val typ = Simple_Syntax.read_typ;
val typeT = Syntax.typeT;
val spropT = Syntax.spropT;
in
--- a/src/HOL/Tools/Function/function.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/Function/function.ML Mon Nov 02 13:43:50 2009 -0800
@@ -44,12 +44,12 @@
[Simplifier.simp_add,
Nitpick_Psimps.add]
-fun note_theorem ((name, atts), ths) =
- LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
+fun note_theorem ((binding, atts), ths) =
+ LocalTheory.note Thm.generatedK ((binding, atts), ths)
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
+fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
let
val spec = post simps
|> map (apfst (apsnd (fn ats => moreatts @ ats)))
@@ -62,7 +62,8 @@
val simps_by_f = sort saved_simps
fun add_for_f fname simps =
- note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
+ note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
+ #> snd
in
(saved_simps,
fold2 add_for_f fnames simps_by_f lthy)
@@ -89,19 +90,22 @@
cont (Thm.close_derivation proof)
val fnames = map (fst o fst) fixes
- val qualify = Long_Name.qualify defname
+ fun qualify n = Binding.name n
+ |> Binding.qualify true defname
+ val conceal_partial = if partials then I else Binding.conceal
+
val addsmps = add_simps fnames post sort_cont
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps (Binding.qualify false "partial") "psimps"
- psimp_attribs psimps
- ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
- ||>> note_theorem ((qualify "pinduct",
+ |> addsmps (conceal_partial o Binding.qualify false "partial")
+ "psimps" conceal_partial psimp_attribs psimps
+ ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
+ ||>> note_theorem ((conceal_partial (qualify "pinduct"),
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
- ||>> note_theorem ((qualify "termination", []), [termination])
+ ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination])
||> (snd o note_theorem ((qualify "cases",
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
@@ -147,10 +151,11 @@
full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
- val qualify = Long_Name.qualify defname;
+ fun qualify n = Binding.name n
+ |> Binding.qualify true defname
in
lthy
- |> add_simps I "simps" simp_attribs tsimps |> snd
+ |> add_simps I "simps" I simp_attribs tsimps |> snd
|> note_theorem
((qualify "induct",
[Attrib.internal (K (Rule_Cases.case_names case_names))]),
--- a/src/HOL/Tools/Function/function_common.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/Function/function_common.ML Mon Nov 02 13:43:50 2009 -0800
@@ -65,8 +65,9 @@
defname : string,
(* contains no logical entities: invariant under morphisms *)
- add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list
- -> local_theory -> thm list * local_theory,
+ add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+ Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+
case_names : string list,
fs : term list,
--- a/src/HOL/Tools/Function/mutual.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/Function/mutual.ML Mon Nov 02 13:43:50 2009 -0800
@@ -148,7 +148,8 @@
val ((f, (_, f_defthm)), lthy') =
LocalTheory.define Thm.internalK
((Binding.name fname, mixfix),
- (apfst Binding.conceal Attrib.empty_binding, Term.subst_bound (fsum, f_def))) lthy
+ ((Binding.conceal (Binding.name (fname ^ "_def")), []),
+ Term.subst_bound (fsum, f_def))) lthy
in
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
f=SOME f, f_defthm=SOME f_defthm },
--- a/src/HOL/Tools/record.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/record.ML Mon Nov 02 13:43:50 2009 -0800
@@ -262,7 +262,7 @@
infixr 0 ==>;
val op $$ = Term.list_comb;
-val op :== = PrimitiveDefs.mk_defpair;
+val op :== = Primitive_Defs.mk_defpair;
val op === = Trueprop o HOLogic.mk_eq;
val op ==> = Logic.mk_implies;
--- a/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 02 13:43:50 2009 -0800
@@ -15,8 +15,8 @@
open Proofterm;
-val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
- Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
+val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
+ Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
(** eliminate meta-equality rules **)
--- a/src/HOL/Tools/typedef.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Tools/typedef.ML Mon Nov 02 13:43:50 2009 -0800
@@ -115,7 +115,7 @@
theory
|> Sign.add_consts_i [(name, setT', NoSyn)]
|> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
- (PrimitiveDefs.mk_defpair (setC, set)))]
+ (Primitive_Defs.mk_defpair (setC, set)))]
|-> (fn [th] => pair (SOME th))
else (NONE, theory);
fun contract_def NONE th = th
--- a/src/HOL/Typerep.thy Mon Nov 02 12:26:23 2009 -0800
+++ b/src/HOL/Typerep.thy Mon Nov 02 13:43:50 2009 -0800
@@ -29,7 +29,7 @@
| typerep_tr' _ T ts = raise Match;
in
Sign.add_syntax_i
- [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
+ [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
#> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
#> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
end
--- a/src/Pure/Isar/auto_bind.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/auto_bind.ML Mon Nov 02 13:43:50 2009 -0800
@@ -14,7 +14,7 @@
val no_facts: (indexname * term option) list
end;
-structure AutoBind: AUTO_BIND =
+structure Auto_Bind: AUTO_BIND =
struct
(** bindings **)
--- a/src/Pure/Isar/constdefs.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/constdefs.ML Mon Nov 02 13:43:50 2009 -0800
@@ -60,7 +60,7 @@
val ctxt = ProofContext.init thy;
val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
- in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
+ in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
--- a/src/Pure/Isar/element.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/element.ML Mon Nov 02 13:43:50 2009 -0800
@@ -294,7 +294,7 @@
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
gen_witness_proof (fn after_qed' => fn propss =>
Proof.map_context (K goal_ctxt)
- #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+ #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
(fn wits => fn _ => after_qed wits) wit_propss [];
--- a/src/Pure/Isar/isar_cmd.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/isar_cmd.ML Mon Nov 02 13:43:50 2009 -0800
@@ -324,7 +324,7 @@
val print_context = Toplevel.keep Toplevel.print_state_context;
fun print_theory verbose = Toplevel.unknown_theory o
- Toplevel.keep (Pretty.writeln o ProofDisplay.pretty_full_theory verbose o Toplevel.theory_of);
+ 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);
@@ -346,8 +346,8 @@
val print_theorems_theory = Toplevel.keep (fn state =>
Toplevel.theory_of state |>
(case Toplevel.previous_context_of state of
- SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
- | NONE => ProofDisplay.print_theorems));
+ SOME prev => Proof_Display.print_theorems_diff (ProofContext.theory_of prev)
+ | NONE => Proof_Display.print_theorems));
val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
@@ -408,7 +408,7 @@
in Present.display_graph gr end);
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+ Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
(* find unused theorems *)
@@ -419,7 +419,7 @@
val ctxt = Toplevel.context_of state;
fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
in
- ThmDeps.unused_thms
+ Thm_Deps.unused_thms
(case opt_range of
NONE => (Theory.parents_of thy, [thy])
| SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
@@ -460,11 +460,11 @@
val prop = Thm.full_prop_of thm;
val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
in
- ProofSyntax.pretty_proof ctxt
+ Proof_Syntax.pretty_proof ctxt
(if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
end
| SOME args => Pretty.chunks
- (map (ProofSyntax.pretty_proof_of (Proof.context_of state) full)
+ (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
(Proof.get_thmss state args)));
fun string_of_prop state s =
--- a/src/Pure/Isar/isar_syn.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML Mon Nov 02 13:43:50 2009 -0800
@@ -685,7 +685,7 @@
OuterSyntax.command "proof" "backward proof"
(K.tag_proof K.prf_block)
(Scan.option Method.parse >> (fn m => Toplevel.print o
- Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o
+ Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
Toplevel.skip_proof (fn i => i + 1)));
@@ -720,7 +720,7 @@
val _ =
OuterSyntax.command "back" "backtracking of proof command"
(K.tag_proof K.prf_script)
- (Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I));
+ (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
(* nested commands *)
--- a/src/Pure/Isar/local_defs.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/local_defs.ML Mon Nov 02 13:43:50 2009 -0800
@@ -47,11 +47,11 @@
quote (Syntax.string_of_term ctxt eq));
val ((lhs, _), eq') = eq
|> Sign.no_vars (Syntax.pp ctxt)
- |> PrimitiveDefs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
+ |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
handle TERM (msg, _) => err msg | ERROR msg => err msg;
in (Term.dest_Free (Term.head_of lhs), eq') end;
-val abs_def = PrimitiveDefs.abs_def #>> Term.dest_Free;
+val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free;
fun mk_def ctxt args =
let
--- a/src/Pure/Isar/local_syntax.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/local_syntax.ML Mon Nov 02 13:43:50 2009 -0800
@@ -21,7 +21,7 @@
val extern_term: T -> term -> term
end;
-structure LocalSyntax: LOCAL_SYNTAX =
+structure Local_Syntax: LOCAL_SYNTAX =
struct
(* datatype T *)
--- a/src/Pure/Isar/local_theory.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/local_theory.ML Mon Nov 02 13:43:50 2009 -0800
@@ -150,9 +150,9 @@
fun target_result f lthy =
let
val (res, ctxt') = target_of lthy
- |> ContextPosition.set_visible false
+ |> Context_Position.set_visible false
|> f
- ||> ContextPosition.restore_visible lthy;
+ ||> Context_Position.restore_visible lthy;
val thy' = ProofContext.theory_of ctxt';
val lthy' = lthy
|> map_target (K ctxt')
--- a/src/Pure/Isar/obtain.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/obtain.ML Mon Nov 02 13:43:50 2009 -0800
@@ -129,7 +129,7 @@
val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
(*obtain statements*)
- val thesisN = Name.variant xs AutoBind.thesisN;
+ val thesisN = Name.variant xs Auto_Bind.thesisN;
val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
val asm_frees = fold Term.add_frees asm_props [];
@@ -142,7 +142,7 @@
Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))
|> Library.curry Logic.list_rename_params xs;
val obtain_prop =
- Logic.list_rename_params ([AutoBind.thesisN],
+ Logic.list_rename_params ([Auto_Bind.thesisN],
Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
fun after_qed _ =
@@ -189,7 +189,7 @@
val thy = ProofContext.theory_of ctxt;
val cert = Thm.cterm_of thy;
- val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt AutoBind.thesisN;
+ val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
val rule =
(case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
@@ -273,7 +273,7 @@
val ctxt = Proof.context_of state;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
- val (thesis_var, thesis) = #1 (bind_judgment ctxt AutoBind.thesisN);
+ val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt;
fun guess_context raw_rule state' =
@@ -293,12 +293,12 @@
|> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
(obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
- |> Proof.bind_terms AutoBind.no_facts
+ |> Proof.bind_terms Auto_Bind.no_facts
end;
val goal = Var (("guess", 0), propT);
fun print_result ctxt' (k, [(s, [_, th])]) =
- ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
+ Proof_Display.print_results int ctxt' (k, [(s, [th])]);
val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
(fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
@@ -307,7 +307,7 @@
state
|> Proof.enter_forward
|> Proof.begin_block
- |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
+ |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (apsnd (rpair I))
"guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
--- a/src/Pure/Isar/proof.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof.ML Mon Nov 02 13:43:50 2009 -0800
@@ -225,7 +225,7 @@
fun put_facts facts =
map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
- put_thms true (AutoBind.thisN, facts);
+ put_thms true (Auto_Bind.thisN, facts);
fun these_factss more_facts (named_factss, state) =
(named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
@@ -710,7 +710,7 @@
in
state'
|> assume_i assumptions
- |> bind_terms AutoBind.no_facts
+ |> bind_terms Auto_Bind.no_facts
|> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
end;
@@ -941,7 +941,7 @@
local
fun gen_have prep_att prepp before_qed after_qed stmt int =
- local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt;
+ local_goal (Proof_Display.print_results int) prep_att prepp "have" before_qed after_qed stmt;
fun gen_show prep_att prepp before_qed after_qed stmt int state =
let
@@ -949,14 +949,14 @@
val rule = Unsynchronized.ref (NONE: thm option);
fun fail_msg ctxt =
"Local statement will fail to refine any pending goal" ::
- (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
+ (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
|> cat_lines;
fun print_results ctxt res =
- if ! testing then () else ProofDisplay.print_results int ctxt res;
+ if ! testing then () else Proof_Display.print_results int ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
- else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
+ else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
else ();
val test_proof =
try (local_skip_proof true)
@@ -1026,10 +1026,10 @@
val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
(Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
- fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
- fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+ 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]);
val after_qed' = (after_local', after_global');
- val this_name = ProofContext.full_name goal_ctxt (Binding.name AutoBind.thisN);
+ val this_name = ProofContext.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
val result_ctxt =
state
--- a/src/Pure/Isar/proof_context.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof_context.ML Mon Nov 02 13:43:50 2009 -0800
@@ -166,7 +166,7 @@
Ctxt of
{mode: mode, (*inner syntax mode*)
naming: Name_Space.naming, (*local naming conventions*)
- syntax: LocalSyntax.T, (*local syntax*)
+ syntax: Local_Syntax.T, (*local syntax*)
consts: Consts.T * Consts.T, (*local/global consts*)
facts: Facts.T, (*local facts*)
cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*)
@@ -181,7 +181,7 @@
(
type T = ctxt;
fun init thy =
- make_ctxt (mode_default, local_naming, LocalSyntax.init thy,
+ make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
(Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
);
@@ -230,9 +230,9 @@
val full_name = Name_Space.full_name o naming_of;
val syntax_of = #syntax o rep_context;
-val syn_of = LocalSyntax.syn_of o syntax_of;
-val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
-val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
+val syn_of = Local_Syntax.syn_of o syntax_of;
+val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
+val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
val consts_of = #1 o #consts o rep_context;
val const_syntax_name = Consts.syntax_name o consts_of;
@@ -247,7 +247,7 @@
(* theory transfer *)
fun transfer_syntax thy =
- map_syntax (LocalSyntax.rebuild thy) #>
+ map_syntax (Local_Syntax.rebuild thy) #>
map_consts (fn consts as (local_consts, global_consts) =>
let val thy_consts = Sign.consts_of thy in
if Consts.eq_consts (thy_consts, global_consts) then consts
@@ -710,8 +710,8 @@
in
t
|> Sign.extern_term (Consts.extern_early consts) thy
- |> LocalSyntax.extern_term syntax
- |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (LocalSyntax.syn_of syntax)
+ |> Local_Syntax.extern_term syntax
+ |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (Local_Syntax.syn_of syntax)
(not (PureThy.old_appl_syntax thy))
end;
@@ -773,8 +773,8 @@
fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
-val auto_bind_goal = auto_bind AutoBind.goal;
-val auto_bind_facts = auto_bind AutoBind.facts;
+val auto_bind_goal = auto_bind Auto_Bind.goal;
+val auto_bind_facts = auto_bind Auto_Bind.facts;
(* match_bind(_i) *)
@@ -932,7 +932,7 @@
let
val pos = Binding.pos_of b;
val name = full_name ctxt b;
- val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
+ val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
val facts = PureThy.name_thmss false pos name raw_facts;
fun app (th, attrs) x =
@@ -945,9 +945,9 @@
fun put_thms do_props thms ctxt = ctxt
|> map_naming (K local_naming)
- |> ContextPosition.set_visible false
+ |> Context_Position.set_visible false
|> update_thms do_props (apfst Binding.name thms)
- |> ContextPosition.restore_visible ctxt
+ |> Context_Position.restore_visible ctxt
|> restore_naming ctxt;
end;
@@ -1029,7 +1029,7 @@
fun notation add mode args ctxt =
ctxt |> map_syntax
- (LocalSyntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
+ (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
fun target_notation add mode args phi =
let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
@@ -1083,9 +1083,9 @@
val ctxt'' =
ctxt'
|> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
- |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
+ |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map prep_mixfix);
val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
- ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
+ Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
in (xs', ctxt'') end;
end;
@@ -1316,7 +1316,7 @@
val prt_term = Syntax.pretty_term ctxt;
(*structures*)
- val structs = LocalSyntax.structs_of (syntax_of ctxt);
+ val structs = Local_Syntax.structs_of (syntax_of ctxt);
val prt_structs = if null structs then []
else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
Pretty.commas (map Pretty.str structs))];
--- a/src/Pure/Isar/proof_display.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof_display.ML Mon Nov 02 13:43:50 2009 -0800
@@ -21,7 +21,7 @@
val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
end
-structure ProofDisplay: PROOF_DISPLAY =
+structure Proof_Display: PROOF_DISPLAY =
struct
(* toplevel pretty printing *)
--- a/src/Pure/Isar/proof_node.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/proof_node.ML Mon Nov 02 13:43:50 2009 -0800
@@ -15,36 +15,36 @@
val apply: (Proof.state -> Proof.state) -> T -> T
end;
-structure ProofNode: PROOF_NODE =
+structure Proof_Node: PROOF_NODE =
struct
(* datatype *)
-datatype T = ProofNode of
+datatype T = Proof_Node of
(Proof.state * (*first result*)
Proof.state Seq.seq) * (*alternative results*)
int; (*linear proof position*)
-fun init st = ProofNode ((st, Seq.empty), 0);
+fun init st = Proof_Node ((st, Seq.empty), 0);
-fun current (ProofNode ((st, _), _)) = st;
-fun position (ProofNode (_, n)) = n;
+fun current (Proof_Node ((st, _), _)) = st;
+fun position (Proof_Node (_, n)) = n;
(* backtracking *)
-fun back (ProofNode ((_, stq), n)) =
+fun back (Proof_Node ((_, stq), n)) =
(case Seq.pull stq of
NONE => error "back: no alternatives"
- | SOME res => ProofNode (res, n));
+ | SOME res => Proof_Node (res, n));
(* apply transformer *)
-fun applys f (ProofNode ((st, _), n)) =
+fun applys f (Proof_Node ((st, _), n)) =
(case Seq.pull (f st) of
NONE => error "empty result sequence -- proof command failed"
- | SOME res => ProofNode (res, n + 1));
+ | SOME res => Proof_Node (res, n + 1));
fun apply f = applys (Seq.single o f);
--- a/src/Pure/Isar/specification.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/specification.ML Mon Nov 02 13:43:50 2009 -0800
@@ -67,7 +67,7 @@
(* diagnostics *)
fun print_consts _ _ [] = ()
- | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
+ | print_consts ctxt pred cs = Pretty.writeln (Proof_Display.pretty_consts ctxt pred cs);
(* prepare specification *)
@@ -267,7 +267,7 @@
((name, map attrib atts),
bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
val (res, lthy') = lthy |> LocalTheory.notes kind facts;
- val _ = ProofDisplay.print_results true lthy' ((kind, ""), res);
+ val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
in (res, lthy') end;
val theorems = gen_theorems (K I) (K I);
@@ -298,7 +298,7 @@
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
- val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
+ val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
@@ -323,7 +323,7 @@
val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
- |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
+ |> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
|-> (fn ths => ProofContext.note_thmss Thm.assumptionK
[((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
@@ -357,19 +357,19 @@
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
|> (fn (res, lthy') =>
if Binding.is_empty name andalso null atts then
- (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
+ (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
else
let
val ([(res_name, _)], lthy'') = lthy'
|> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
- val _ = ProofDisplay.print_results true lthy' ((kind, res_name), res);
+ val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
in lthy'' end)
|> after_qed results'
end;
in
goal_ctxt
|> ProofContext.note_thmss Thm.assumptionK
- [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
+ [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
--- a/src/Pure/Isar/toplevel.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Isar/toplevel.ML Mon Nov 02 13:43:50 2009 -0800
@@ -72,7 +72,7 @@
val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
val proof: (Proof.state -> Proof.state) -> transition -> transition
- val actual_proof: (ProofNode.T -> ProofNode.T) -> transition -> transition
+ val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
val skip_proof: (int -> int) -> transition -> transition
val skip_proof_to_theory: (int -> bool) -> transition -> transition
val get_id: transition -> string option
@@ -121,7 +121,7 @@
datatype node =
Theory of generic_theory * Proof.context option
(*theory with presentation context*) |
- Proof of ProofNode.T * ((Proof.context -> generic_theory) * generic_theory)
+ Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
(*proof node, finish, original theory*) |
SkipProof of int * (generic_theory * generic_theory);
(*proof depth, resulting theory, original theory*)
@@ -130,7 +130,7 @@
val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
fun cases_node f _ (Theory (gthy, _)) = f gthy
- | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf)
+ | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
| cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
val context_node = cases_node Context.proof_of Proof.context_of;
@@ -148,7 +148,7 @@
fun level (State (NONE, _)) = 0
| level (State (SOME (Theory _, _), _)) = 0
- | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (ProofNode.current prf)
+ | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
| level (State (SOME (SkipProof (d, _), _), _)) = d + 1; (*different notion of proof depth!*)
fun str_of_state (State (NONE, _)) = "at top level"
@@ -184,7 +184,7 @@
fun proof_position_of state =
(case node_of state of
- Proof (prf, _) => ProofNode.position prf
+ Proof (prf, _) => Proof_Node.position prf
| _ => raise UNDEF);
val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
@@ -207,7 +207,7 @@
NONE => []
| SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
| SOME (Proof (prf, _)) =>
- Proof.pretty_state (ProofNode.position prf) (ProofNode.current prf)
+ Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
| SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
|> Pretty.markup_chunks Markup.state |> Pretty.writeln;
@@ -450,7 +450,7 @@
fun end_proof f = transaction (fn int =>
(fn Proof (prf, (finish, _)) =>
- let val state = ProofNode.current prf in
+ let val state = Proof_Node.current prf in
if can (Proof.assert_bottom true) state then
let
val ctxt' = f int state;
@@ -475,7 +475,7 @@
else ();
if skip andalso not schematic then
SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
- else Proof (ProofNode.init prf, (finish gthy, gthy))
+ else Proof (Proof_Node.init prf, (finish gthy, gthy))
end
| _ => raise UNDEF));
@@ -499,12 +499,12 @@
| _ => raise UNDEF));
val present_proof = present_transaction (fn _ =>
- (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
+ (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
| skip as SkipProof _ => skip
| _ => raise UNDEF));
fun proofs' f = transaction (fn int =>
- (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
+ (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
| skip as SkipProof _ => skip
| _ => raise UNDEF));
@@ -654,7 +654,7 @@
Future.fork_pri ~1 (fn () =>
let val (states, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
- => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
+ => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev))
|> fold_map command_result body_trs
||> command (end_tr |> set_print false);
in (states, presentation_context_of result_state) end))
--- a/src/Pure/Proof/extraction.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Proof/extraction.ML Mon Nov 02 13:43:50 2009 -0800
@@ -300,7 +300,7 @@
val rtypes = map fst types;
val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
val thy' = add_syntax thy;
- val rd = ProofSyntax.read_proof thy' false
+ val rd = Proof_Syntax.read_proof thy' false;
in fn (thm, (vs, s1, s2)) =>
let
val name = Thm.get_name thm;
--- a/src/Pure/Proof/proof_syntax.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Proof/proof_syntax.ML Mon Nov 02 13:43:50 2009 -0800
@@ -19,7 +19,7 @@
val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
-structure ProofSyntax : PROOF_SYNTAX =
+structure Proof_Syntax : PROOF_SYNTAX =
struct
open Proofterm;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Nov 02 13:43:50 2009 -0800
@@ -658,7 +658,7 @@
fun strings_of_thm (thy, name) =
map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
- val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
+ val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
in
case (thyname, objtype) of
(_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
--- a/src/Pure/Syntax/simple_syntax.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Syntax/simple_syntax.ML Mon Nov 02 13:43:50 2009 -0800
@@ -11,7 +11,7 @@
val read_prop: string -> term
end;
-structure SimpleSyntax: SIMPLE_SYNTAX =
+structure Simple_Syntax: SIMPLE_SYNTAX =
struct
(* scanning tokens *)
--- a/src/Pure/Thy/thm_deps.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Thy/thm_deps.ML Mon Nov 02 13:43:50 2009 -0800
@@ -10,7 +10,7 @@
val unused_thms: theory list * theory list -> (string * thm) list
end;
-structure ThmDeps: THM_DEPS =
+structure Thm_Deps: THM_DEPS =
struct
(* thm_deps *)
--- a/src/Pure/Thy/thy_output.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Thy/thy_output.ML Mon Nov 02 13:43:50 2009 -0800
@@ -478,7 +478,7 @@
val ctxt' = Variable.auto_fixes eq ctxt;
in ProofContext.pretty_term_abbrev ctxt' eq end;
-fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
+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);
--- a/src/Pure/Tools/xml_syntax.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/Tools/xml_syntax.ML Mon Nov 02 13:43:50 2009 -0800
@@ -17,7 +17,7 @@
val proof_of_xml: XML.tree -> Proofterm.proof
end;
-structure XMLSyntax : XML_SYNTAX =
+structure XML_Syntax : XML_SYNTAX =
struct
(**** XML output ****)
--- a/src/Pure/conjunction.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/conjunction.ML Mon Nov 02 13:43:50 2009 -0800
@@ -30,7 +30,7 @@
(** abstract syntax **)
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
-val read_prop = certify o SimpleSyntax.read_prop;
+val read_prop = certify o Simple_Syntax.read_prop;
val true_prop = certify Logic.true_prop;
val conjunction = certify Logic.conjunction;
--- a/src/Pure/context_position.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/context_position.ML Mon Nov 02 13:43:50 2009 -0800
@@ -12,7 +12,7 @@
val report_visible: Proof.context -> Markup.T -> Position.T -> unit
end;
-structure ContextPosition: CONTEXT_POSITION =
+structure Context_Position: CONTEXT_POSITION =
struct
structure Data = ProofDataFun
--- a/src/Pure/drule.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/drule.ML Mon Nov 02 13:43:50 2009 -0800
@@ -450,7 +450,7 @@
(*** Meta-Rewriting Rules ***)
-val read_prop = certify o SimpleSyntax.read_prop;
+val read_prop = certify o Simple_Syntax.read_prop;
fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
--- a/src/Pure/primitive_defs.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/primitive_defs.ML Mon Nov 02 13:43:50 2009 -0800
@@ -12,7 +12,7 @@
val mk_defpair: term * term -> string * term
end;
-structure PrimitiveDefs: PRIMITIVE_DEFS =
+structure Primitive_Defs: PRIMITIVE_DEFS =
struct
fun term_kind (Const _) = "existing constant "
--- a/src/Pure/pure_setup.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/pure_setup.ML Mon Nov 02 13:43:50 2009 -0800
@@ -22,13 +22,13 @@
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
toplevel_pp ["Position", "T"] "Pretty.position";
toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
-toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
-toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
-toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
-toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
+toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
+toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
+toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
+toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
toplevel_pp ["Context", "theory"] "Context.pretty_thy";
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
-toplevel_pp ["Context", "Proof", "context"] "ProofDisplay.pp_context";
+toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
--- a/src/Pure/pure_thy.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/pure_thy.ML Mon Nov 02 13:43:50 2009 -0800
@@ -227,8 +227,8 @@
(*** Pure theory syntax and logical content ***)
-val typ = SimpleSyntax.read_typ;
-val prop = SimpleSyntax.read_prop;
+val typ = Simple_Syntax.read_typ;
+val prop = Simple_Syntax.read_prop;
val typeT = Syntax.typeT;
val spropT = Syntax.spropT;
--- a/src/Pure/sign.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/Pure/sign.ML Mon Nov 02 13:43:50 2009 -0800
@@ -392,7 +392,7 @@
let val ((lhs, rhs), _) = tm
|> no_vars (Syntax.pp ctxt)
|> Logic.strip_imp_concl
- |> PrimitiveDefs.dest_def ctxt Term.is_Const (K false) (K false)
+ |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
in (Term.dest_Const (Term.head_of lhs), rhs) end
handle TERM (msg, _) => error msg;
--- a/src/ZF/Tools/datatype_package.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/ZF/Tools/datatype_package.ML Mon Nov 02 13:43:50 2009 -0800
@@ -108,7 +108,7 @@
let val ncon = length con_ty_list (*number of constructors*)
fun mk_def (((id,T,syn), name, args, prems), kcon) =
(*kcon is index of constructor*)
- PrimitiveDefs.mk_defpair (list_comb (Const (full_name name, T), args),
+ Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
mk_inject npart kpart
(mk_inject ncon kcon (mk_tuple args)))
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
@@ -157,7 +157,7 @@
val case_const = Const (case_name, case_typ);
val case_tm = list_comb (case_const, case_args);
- val case_def = PrimitiveDefs.mk_defpair
+ val case_def = Primitive_Defs.mk_defpair
(case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
@@ -232,7 +232,7 @@
val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
val recursor_def =
- PrimitiveDefs.mk_defpair
+ Primitive_Defs.mk_defpair
(recursor_tm,
@{const Univ.Vrecursor} $
absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
--- a/src/ZF/Tools/inductive_package.ML Mon Nov 02 12:26:23 2009 -0800
+++ b/src/ZF/Tools/inductive_package.ML Mon Nov 02 13:43:50 2009 -0800
@@ -156,7 +156,7 @@
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
(*The individual sets must already be declared*)
- val axpairs = map PrimitiveDefs.mk_defpair
+ val axpairs = map Primitive_Defs.mk_defpair
((big_rec_tm, fp_rhs) ::
(case parts of
[_] => [] (*no mutual recursion*)