# 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;