# HG changeset patch
# User wenzelm
# Date 1433789622 -7200
# Node ID 0c9d2a4f589d1a5556161dd789fead2ed80e8359
# Parent  76359ff1090f4f2070c168d9d71a04748d7b326a
clarified Proof_Context.cert_propp/read_propp;
tuned;

diff -r 76359ff1090f -r 0c9d2a4f589d src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Jun 08 19:38:08 2015 +0200
+++ b/src/Pure/Isar/element.ML	Mon Jun 08 20:53:42 2015 +0200
@@ -278,10 +278,10 @@
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness #> Seq.hd end;
 
-fun proof_local cmd goal_ctxt int after_qed' propss =
+fun proof_local cmd goal_ctxt int after_qed' propp =
   Proof.map_context (K goal_ctxt) #>
-  Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp cmd NONE
-    after_qed' (map (pair Thm.empty_binding) propss);
+  Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE
+    after_qed' (map (pair Thm.empty_binding) propp);
 
 in
 
diff -r 76359ff1090f -r 0c9d2a4f589d src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Jun 08 19:38:08 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 08 20:53:42 2015 +0200
@@ -118,14 +118,17 @@
     val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
-    val ((propss, binds), props_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
-    val props = flat propss;
+    val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
+    val asm_props = flat asm_propss;
+    val asms_ctxt = fix_ctxt
+      |> fold Variable.declare_term asm_props
+      |> Proof_Context.bind_terms binds;
     val asms =
       map (fn ((b, raw_atts), _) => (b, map (prep_att ctxt) raw_atts)) raw_asms ~~
-      unflat propss (map (rpair []) props);
+      unflat asm_propss (map (rpair []) asm_props);
 
     (*obtain params*)
-    val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' props_ctxt;
+    val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
     val params = map Free (xs' ~~ Ts);
     val cparams = map (Thm.cterm_of params_ctxt) params;
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
@@ -146,7 +149,7 @@
     val that_name = if name = "" then thatN else name;
     val that_prop =
       Logic.list_rename_params xs
-        (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
+        (fold_rev Logic.all params (Logic.list_implies (asm_props, thesis)));
     val obtain_prop =
       Logic.list_rename_params [Auto_Bind.thesisN]
         (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
@@ -174,8 +177,8 @@
 
 in
 
-val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.bind_propp;
-val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.bind_propp_cmd;
+val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.read_propp;
 
 end;
 
@@ -319,7 +322,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) (pair o rpair [])
+    |> Proof.local_goal print_result (K I) (K (rpair []))
       "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
     |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
         Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
diff -r 76359ff1090f -r 0c9d2a4f589d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jun 08 19:38:08 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jun 08 20:53:42 2015 +0200
@@ -91,7 +91,7 @@
   val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (context -> 'a -> attribute) ->
-    ('b list -> context -> (term list list * (indexname * term) list) * context) ->
+    (context -> 'b list -> (term list list * (indexname * term) list)) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
     ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text_range option * bool -> state -> state
@@ -910,19 +910,21 @@
 
 in
 
-fun generic_goal prepp kind before_qed after_qed raw_propp state =
+fun generic_goal prep_propp kind before_qed after_qed propp state =
   let
     val ctxt = context_of state;
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val ((propss, binds), goal_state) =
+    val (propss, binds) = prep_propp ctxt propp;
+    val props = flat propss;
+
+    val goal_state =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
-      |> map_context_result (prepp raw_propp);
-    val props = flat propss;
+      |> map_context (fold Variable.auto_fixes props #> Proof_Context.bind_terms binds);
     val goal_ctxt = context_of goal_state;
 
     val vars = implicit_vars props;
@@ -972,7 +974,7 @@
 
 (* local goals *)
 
-fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
+fun local_goal print_results prep_att prep_propp kind before_qed after_qed stmt state =
   let
     val ((names, attss), propp) =
       Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
@@ -983,7 +985,8 @@
       #> after_qed results;
   in
     state
-    |> generic_goal prepp kind before_qed (after_qed', K I) propp
+    |> map_context (Variable.set_body true)
+    |> generic_goal prep_propp kind before_qed (after_qed', K I) propp
     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
@@ -998,21 +1001,13 @@
 
 (* global goals *)
 
-fun global_goal prepp before_qed after_qed propp =
-  let
-    fun prepp' args ctxt1 =
-      let
-        val ((propss, binds), ctxt2) = ctxt1
-          |> Proof_Context.set_mode Proof_Context.mode_schematic
-          |> prepp args;
-        val ctxt3 = ctxt2
-          |> (fold o fold) Variable.auto_fixes propss
-          |> Proof_Context.restore_mode ctxt1;
-      in ((propss, binds), ctxt3) end;
-  in init #> generic_goal prepp' "" before_qed (K I, after_qed) propp end;
+fun global_goal prep_propp before_qed after_qed propp =
+  init
+  #> generic_goal (prep_propp o Proof_Context.set_mode Proof_Context.mode_schematic) ""
+    before_qed (K I, after_qed) propp;
 
-val theorem = global_goal Proof_Context.bind_propp;
-val theorem_cmd = global_goal Proof_Context.bind_propp_cmd;
+val theorem = global_goal Proof_Context.cert_propp;
+val theorem_cmd = global_goal Proof_Context.read_propp;
 
 fun global_qeds arg =
   end_proof true arg
@@ -1061,11 +1056,11 @@
 
 local
 
-fun gen_have prep_att prepp before_qed after_qed stmt int =
+fun gen_have prep_att prep_propp before_qed after_qed stmt int =
   local_goal (Proof_Display.print_results int (Position.thread_data ()))
-    prep_att prepp "have" before_qed after_qed stmt;
+    prep_att prep_propp "have" before_qed after_qed stmt;
 
-fun gen_show prep_att prepp before_qed after_qed stmt int state =
+fun gen_show prep_att prep_propp before_qed after_qed stmt int state =
   let
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
@@ -1096,7 +1091,7 @@
       #> after_qed results;
   in
     state
-    |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
+    |> local_goal print_results prep_att prep_propp "show" before_qed after_qed' stmt
     |> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
         Exn.Res _ => goal_state
@@ -1105,10 +1100,10 @@
 
 in
 
-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;
+val have = gen_have (K I) Proof_Context.cert_propp;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp;
+val show = gen_show (K I) Proof_Context.cert_propp;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp;
 
 end;
 
diff -r 76359ff1090f -r 0c9d2a4f589d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jun 08 19:38:08 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jun 08 20:53:42 2015 +0200
@@ -114,10 +114,10 @@
     term list * Proof.context
   val match_bind_cmd: bool -> (string list * string) list -> Proof.context ->
     term list * Proof.context
-  val bind_propp: (term * term list) list list -> Proof.context ->
-    (term list list * (indexname * term) list) * Proof.context
-  val bind_propp_cmd: (string * string list) list list -> Proof.context ->
-    (term list list * (indexname * term) list) * Proof.context
+  val cert_propp: Proof.context -> (term * term list) list list ->
+    (term list list * (indexname * term) list)
+  val read_propp: Proof.context -> (string * string list) list list ->
+    (term list list * (indexname * term) list)
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
   val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
@@ -884,22 +884,20 @@
 
 local
 
-fun gen_bind_propp prep_props raw_args ctxt =
+fun prep_propp prep_props ctxt raw_args =
   let
     val props = prep_props ctxt (maps (map fst) raw_args);
-    val ctxt' = fold Variable.declare_term props ctxt;
+    val props_ctxt = fold Variable.declare_term props ctxt;
+    val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args;
 
-    val patss = maps (map (prep_props (set_mode mode_pattern ctxt') o snd)) raw_args;
     val propps = unflat raw_args (props ~~ patss);
-    val binds = (maps o maps) (simult_matches ctxt') propps;
-
-    val propss = map (map fst) propps;
-  in ((propss, binds), bind_terms binds ctxt') end;
+    val binds = (maps o maps) (simult_matches props_ctxt) propps;
+  in (map (map fst) propps, binds) end;
 
 in
 
-val bind_propp = gen_bind_propp (map o cert_prop);
-val bind_propp_cmd = gen_bind_propp Syntax.read_props;
+val cert_propp = prep_propp (map o cert_prop);
+val read_propp = prep_propp Syntax.read_props;
 
 end;
 
@@ -1160,22 +1158,25 @@
 
 local
 
-fun gen_assms prepp exp args ctxt =
+fun gen_assms prep_propp exp args ctxt =
   let
-    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 (Thm.cterm_of ctxt)) propss ctxt1;
+    val (propss, binds) = prep_propp ctxt (map snd args);
+    val props = flat propss;
   in
-    ctxt2
-    |> auto_bind_facts (flat propss)
-    |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)
+    ctxt
+    |> fold Variable.declare_term props
+    |> tap (Variable.warn_extra_tfrees ctxt)
+    |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
+    |-> (fn premss =>
+      auto_bind_facts props
+      #> bind_terms binds
+      #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
   end;
 
 in
 
-val add_assms = gen_assms bind_propp;
-val add_assms_cmd = gen_assms bind_propp_cmd;
+val add_assms = gen_assms cert_propp;
+val add_assms_cmd = gen_assms read_propp;
 
 end;