# HG changeset patch # User wenzelm # Date 1433682067 -7200 # Node ID 234b7da8542eb905e24730fa3f157a6c3616c1a9 # Parent 528a48f4ad87a13fcfe1b7530c0189a81ec7bbfc tuned signature; diff -r 528a48f4ad87 -r 234b7da8542e src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sun Jun 07 14:36:36 2015 +0200 +++ b/src/Pure/Isar/element.ML Sun Jun 07 15:01:07 2015 +0200 @@ -280,7 +280,7 @@ fun proof_local cmd goal_ctxt int after_qed' propss = Proof.map_context (K goal_ctxt) #> - Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp_i cmd NONE + Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp cmd NONE after_qed' (map (pair Thm.empty_binding) propss); in @@ -473,7 +473,7 @@ val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms; val (_, ctxt') = ctxt |> fold Variable.auto_fixes (maps (map #1 o #2) asms') - |> Proof_Context.add_assms_i Assumption.assume_export asms'; + |> Proof_Context.add_assms Assumption.assume_export asms'; in ctxt' end) | init (Defines defs) = Context.map_proof (fn ctxt => let @@ -483,7 +483,7 @@ in (t', (b, [(t', ps)])) end); val (_, ctxt') = ctxt |> fold Variable.auto_fixes (map #1 asms) - |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms); + |> Proof_Context.add_assms Local_Defs.def_export (map #2 asms); in ctxt' end) | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2; diff -r 528a48f4ad87 -r 234b7da8542e src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Sun Jun 07 14:36:36 2015 +0200 +++ b/src/Pure/Isar/local_defs.ML Sun Jun 07 15:01:07 2015 +0200 @@ -96,7 +96,7 @@ ctxt |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2 |> fold Variable.declare_term eqs - |> Proof_Context.add_assms_i def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs) + |> Proof_Context.add_assms def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs) |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss end; diff -r 528a48f4ad87 -r 234b7da8542e src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Sun Jun 07 14:36:36 2015 +0200 +++ b/src/Pure/Isar/obtain.ML Sun Jun 07 15:01:07 2015 +0200 @@ -119,7 +119,7 @@ (*obtain asms*) val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt; - val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt; + val ((_, bind_ctxt), _) = Proof_Context.bind_propp proppss asms_ctxt; val asm_props = maps (map fst) proppss; val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss; diff -r 528a48f4ad87 -r 234b7da8542e src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sun Jun 07 14:36:36 2015 +0200 +++ b/src/Pure/Isar/proof.ML Sun Jun 07 15:01:07 2015 +0200 @@ -557,8 +557,8 @@ in -val let_bind = gen_bind Proof_Context.match_bind_i; -val let_bind_cmd = gen_bind Proof_Context.match_bind; +val let_bind = gen_bind Proof_Context.match_bind; +val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd; end; @@ -616,8 +616,8 @@ in -val assm = gen_assume Proof_Context.add_assms_i (K I); -val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd; +val assm = gen_assume Proof_Context.add_assms (K I); +val assm_cmd = gen_assume Proof_Context.add_assms_cmd Attrib.attribute_cmd; val assume = assm Assumption.assume_export; val assume_cmd = assm_cmd Assumption.assume_export; val presume = assm Assumption.presume_export; @@ -651,8 +651,8 @@ in -val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i; -val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind; +val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind; +val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind_cmd; end; @@ -1007,8 +1007,8 @@ init #> generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp; -val theorem = global_goal Proof_Context.bind_propp_schematic_i; -val theorem_cmd = global_goal Proof_Context.bind_propp_schematic; +val theorem = global_goal Proof_Context.bind_propp_schematic; +val theorem_cmd = global_goal Proof_Context.bind_propp_schematic_cmd; fun global_qeds arg = end_proof true arg @@ -1101,10 +1101,10 @@ in -val have = gen_have (K I) Proof_Context.bind_propp_i; -val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp; -val show = gen_show (K I) Proof_Context.bind_propp_i; -val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp; +val have = gen_have (K I) Proof_Context.bind_propp; +val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp_cmd; +val show = gen_show (K I) Proof_Context.bind_propp; +val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp_cmd; end; diff -r 528a48f4ad87 -r 234b7da8542e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Jun 07 14:36:36 2015 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun Jun 07 15:01:07 2015 +0200 @@ -108,8 +108,8 @@ val bind_terms: (indexname * term option) list -> Proof.context -> Proof.context val auto_bind_goal: term list -> Proof.context -> Proof.context val auto_bind_facts: term list -> Proof.context -> Proof.context - val match_bind: bool -> (string list * string) list -> Proof.context -> term list * Proof.context - val match_bind_i: bool -> (term list * term) list -> Proof.context -> term list * Proof.context + val match_bind: bool -> (term list * term) list -> Proof.context -> term list * Proof.context + val match_bind_cmd: bool -> (string list * string) list -> Proof.context -> term list * Proof.context val read_propp: (string * string list) list list -> Proof.context -> (term * term list) list list * Proof.context val cert_propp: (term * term list) list list -> Proof.context -> @@ -118,13 +118,13 @@ (term * term list) list list * Proof.context val cert_propp_schematic: (term * term list) list list -> Proof.context -> (term * term list) list list * Proof.context - val bind_propp: (string * string list) list list -> Proof.context -> + val bind_propp: (term * term list) list list -> Proof.context -> (term list list * (Proof.context -> Proof.context)) * Proof.context - val bind_propp_i: (term * term list) list list -> Proof.context -> + val bind_propp_cmd: (string * string list) list list -> Proof.context -> (term list list * (Proof.context -> Proof.context)) * Proof.context - val bind_propp_schematic: (string * string list) list list -> Proof.context -> + val bind_propp_schematic: (term * term list) list list -> Proof.context -> (term list list * (Proof.context -> Proof.context)) * Proof.context - val bind_propp_schematic_i: (term * term list) list list -> Proof.context -> + val bind_propp_schematic_cmd: (string * string list) list list -> Proof.context -> (term list list * (Proof.context -> Proof.context)) * Proof.context val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic @@ -143,10 +143,10 @@ val add_fixes: (binding * typ option * mixfix) list -> Proof.context -> string list * Proof.context val add_assms: Assumption.export -> - (Thm.binding * (string * string list) list) list -> + (Thm.binding * (term * term list) list) list -> Proof.context -> (string * thm list) list * Proof.context - val add_assms_i: Assumption.export -> - (Thm.binding * (term * term list) list) list -> + val add_assms_cmd: Assumption.export -> + (Thm.binding * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context @@ -848,7 +848,7 @@ val auto_bind_facts = auto_bind Auto_Bind.facts; -(* match_bind(_i) *) +(* match_bind *) local @@ -880,8 +880,8 @@ fun read_terms ctxt T = map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt; -val match_bind = gen_bind read_terms; -val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt)); +val match_bind = gen_bind (fn ctxt => fn _ => map (cert_term ctxt)); +val match_bind_cmd = gen_bind read_terms; end; @@ -913,15 +913,15 @@ in -val read_propp = prep_propp mode_default Syntax.read_props; -val cert_propp = prep_propp mode_default (map o cert_prop); +val read_propp = prep_propp mode_default Syntax.read_props; +val cert_propp = prep_propp mode_default (map o cert_prop); val read_propp_schematic = prep_propp mode_schematic Syntax.read_props; val cert_propp_schematic = prep_propp mode_schematic (map o cert_prop); -val bind_propp = gen_bind_propp mode_default Syntax.read_props; -val bind_propp_i = gen_bind_propp mode_default (map o cert_prop); -val bind_propp_schematic = gen_bind_propp mode_schematic Syntax.read_props; -val bind_propp_schematic_i = gen_bind_propp mode_schematic (map o cert_prop); +val bind_propp = gen_bind_propp mode_default (map o cert_prop); +val bind_propp_cmd = gen_bind_propp mode_default Syntax.read_props; +val bind_propp_schematic = gen_bind_propp mode_schematic (map o cert_prop); +val bind_propp_schematic_cmd = gen_bind_propp mode_schematic Syntax.read_props; end; @@ -1198,7 +1198,7 @@ in val add_assms = gen_assms bind_propp; -val add_assms_i = gen_assms bind_propp_i; +val add_assms_cmd = gen_assms bind_propp_cmd; end; diff -r 528a48f4ad87 -r 234b7da8542e src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sun Jun 07 14:36:36 2015 +0200 +++ b/src/Pure/Isar/specification.ML Sun Jun 07 15:01:07 2015 +0200 @@ -372,7 +372,7 @@ in ctxt' |> Variable.auto_fixes asm - |> Proof_Context.add_assms_i Assumption.assume_export + |> Proof_Context.add_assms Assumption.assume_export [((name, [Context_Rules.intro_query NONE]), [(asm, [])])] |>> (fn [(_, [th])] => th) end;