# HG changeset patch
# User wenzelm
# Date 1320355421 -3600
# Node ID 4a027cc86f1a879b60ea7be64de9ce861630d79c
# Parent  8fa859aebc0dc3fea4f771d669f03b005c2a4797
tuned signature -- canonical argument order;

diff -r 8fa859aebc0d -r 4a027cc86f1a src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Nov 03 22:15:47 2011 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Nov 03 22:23:41 2011 +0100
@@ -123,7 +123,7 @@
     val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
-    val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
+    val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
     val asm_props = maps (map fst) proppss;
     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
 
@@ -308,7 +308,7 @@
     |> Proof.begin_block
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
-    |> Proof.local_goal print_result (K I) (apsnd (rpair I))
+    |> Proof.local_goal print_result (K I) (pair o rpair I)
       "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
     |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   end;
diff -r 8fa859aebc0d -r 4a027cc86f1a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Nov 03 22:15:47 2011 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Nov 03 22:23:41 2011 +0100
@@ -84,7 +84,7 @@
   val apply_end: Method.text -> state -> state Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> attribute) ->
-    (context * 'b list -> context * (term list list * (context -> context))) ->
+    ('b list -> context -> (term list list * (context -> context)) * context) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
     ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state
@@ -863,7 +863,7 @@
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
-      |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
+      |> map_context_result (prepp raw_propp);
     val props = flat propss;
 
     val vars = implicit_vars props;
@@ -938,9 +938,13 @@
 
 (* global goals *)
 
-fun global_goal prepp before_qed after_qed propp ctxt =
-  init ctxt
-  |> generic_goal (prepp #> Proof_Context.auto_fixes) "" before_qed (K I, after_qed) propp;
+fun prepp_auto_fixes prepp args =
+  prepp args #>
+  (fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt));
+
+fun global_goal prepp before_qed after_qed propp =
+  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;
diff -r 8fa859aebc0d -r 4a027cc86f1a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Nov 03 22:15:47 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 03 22:23:41 2011 +0100
@@ -93,22 +93,22 @@
   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 read_propp: Proof.context * (string * string list) list list
-    -> Proof.context * (term * term list) list list
-  val cert_propp: Proof.context * (term * term list) list list
-    -> Proof.context * (term * term list) list list
-  val read_propp_schematic: Proof.context * (string * string list) list list
-    -> Proof.context * (term * term list) list list
-  val cert_propp_schematic: Proof.context * (term * term list) list list
-    -> Proof.context * (term * term list) list list
-  val bind_propp: Proof.context * (string * string list) list list
-    -> Proof.context * (term list list * (Proof.context -> Proof.context))
-  val bind_propp_i: Proof.context * (term * term list) list list
-    -> Proof.context * (term list list * (Proof.context -> Proof.context))
-  val bind_propp_schematic: Proof.context * (string * string list) list list
-    -> Proof.context * (term list list * (Proof.context -> Proof.context))
-  val bind_propp_schematic_i: Proof.context * (term * term list) list list
-    -> Proof.context * (term list list * (Proof.context -> 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 ->
+    (term * term list) list list * Proof.context
+  val read_propp_schematic: (string * string list) list list -> Proof.context ->
+    (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 ->
+    (term list list * (Proof.context -> Proof.context)) * Proof.context
+  val bind_propp_i: (term * term 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 ->
+    (term list list * (Proof.context -> Proof.context)) * Proof.context
+  val bind_propp_schematic_i: (term * term list) list list -> Proof.context ->
+    (term list list * (Proof.context -> Proof.context)) * Proof.context
   val fact_tac: thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
   val get_fact: Proof.context -> Facts.ref -> thm list
@@ -124,7 +124,6 @@
     (binding * typ option * mixfix) list * Proof.context
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
-  val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   val add_assms: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
@@ -778,26 +777,27 @@
 
 local
 
-fun prep_propp mode prep_props (context, args) =
+fun prep_propp mode prep_props args context =
   let
     fun prep (_, raw_pats) (ctxt, prop :: props) =
       let val ctxt' = Variable.declare_term prop ctxt
       in ((prop, prep_props (set_mode mode_pattern ctxt') raw_pats), (ctxt', props)) end;
 
-    val (propp, (context', _)) = (fold_map o fold_map) prep args
-      (context, prep_props (set_mode mode context) (maps (map fst) args));
-  in (context', propp) end;
+    val (propp, (context', _)) =
+      (fold_map o fold_map) prep args
+        (context, prep_props (set_mode mode context) (maps (map fst) args));
+  in (propp, context') end;
 
-fun gen_bind_propp mode parse_prop (ctxt, raw_args) =
+fun gen_bind_propp mode parse_prop raw_args ctxt =
   let
-    val (ctxt', args) = prep_propp mode parse_prop (ctxt, raw_args);
+    val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt;
     val binds = flat (flat (map (map (simult_matches ctxt')) args));
     val propss = map (map #1) args;
 
     (*generalize result: context evaluated now, binds added later*)
     val gen = Variable.exportT_terms ctxt' ctxt;
     fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
-  in (ctxt' |> bind_terms (map (apsnd SOME) binds), (propss, gen_binds)) end;
+  in ((propss, gen_binds), ctxt' |> bind_terms (map (apsnd SOME) binds)) end;
 
 in
 
@@ -1038,9 +1038,6 @@
       #> pair xs)
   end;
 
-fun auto_fixes (ctxt, (propss, x)) =
-  ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
-
 
 
 (** assumptions **)
@@ -1050,7 +1047,7 @@
 fun gen_assms prepp exp args ctxt =
   let
     val cert = Thm.cterm_of (theory_of ctxt);
-    val (propss, ctxt1) = swap (prepp (ctxt, map snd args));
+    val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
     val _ = Variable.warn_extra_tfrees ctxt ctxt1;
     val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1;
   in
@@ -1061,8 +1058,8 @@
 
 in
 
-val add_assms = gen_assms (apsnd #1 o bind_propp);
-val add_assms_i = gen_assms (apsnd #1 o bind_propp_i);
+val add_assms = gen_assms bind_propp;
+val add_assms_i = gen_assms bind_propp_i;
 
 end;
 
diff -r 8fa859aebc0d -r 4a027cc86f1a src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Nov 03 22:15:47 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Nov 03 22:23:41 2011 +0100
@@ -308,7 +308,7 @@
         val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
         val prems = Assumption.local_prems_of elems_ctxt ctxt;
         val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
-        val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
+        val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
       in ((prems, stmt, NONE), goal_ctxt) end
   | Element.Obtains obtains =>
       let