Merge

--- a/src/Pure/Isar/obtain.ML	Mon Jun 08 00:25:10 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 08 18:56:04 2015 +0100
@@ -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 proppss asms_ctxt;
+    val ((_, binds), binds_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;
 
@@ -150,7 +150,7 @@
     state
     |> Proof.enter_forward
     |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
-    |> Proof.map_context bind_ctxt
+    |> Proof.map_context (Proof_Context.export_bind_terms binds binds_ctxt)
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume
@@ -289,7 +289,7 @@
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
           (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
             [(Thm.empty_binding, asms)])
-        |> Proof.bind_terms Auto_Bind.no_facts
+        |> Proof.map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
       end;
 
     val goal = Var (("guess", 0), propT);
@@ -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) (pair o rpair I)
+    |> Proof.local_goal print_result (K I) (pair o 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

--- a/src/Pure/Isar/proof.ML	Mon Jun 08 00:25:10 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jun 08 18:56:04 2015 +0100
@@ -19,7 +19,6 @@
   val map_context_result : (context -> 'a * context) -> state -> 'a * state
   val map_contexts: (context -> context) -> state -> state
   val propagate_ml_env: state -> state
-  val bind_terms: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
@@ -92,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 * (context -> context)) * context) ->
+    ('b list -> context -> (term list list * (indexname * term) list) * context) ->
     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
@@ -221,7 +220,6 @@
 fun propagate_ml_env state = map_contexts
   (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
 
-val bind_terms = map_context o Proof_Context.bind_terms;
 val put_thms = map_context oo Proof_Context.put_thms;
 
 
@@ -771,7 +769,7 @@
   in
     state'
     |> assume assumptions
-    |> bind_terms Auto_Bind.no_facts
+    |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
     |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
   end;
 
@@ -918,13 +916,14 @@
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val ((propss, after_ctxt), goal_state) =
+    val ((propss, binds), goal_state) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
       |> map_context_result (prepp raw_propp);
     val props = flat propss;
+    val goal_ctxt = context_of goal_state;
 
     val vars = implicit_vars props;
     val propss' = vars :: propss;
@@ -932,10 +931,10 @@
     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
       |> Thm.cterm_of ctxt
-      |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
+      |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
     val statement = ((kind, pos), propss', Thm.term_of goal);
-    val after_qed' = after_qed |>> (fn after_local =>
-      fn results => map_context after_ctxt #> after_local results);
+    val after_qed' = after_qed |>> (fn after_local => fn results =>
+      map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)

--- a/src/Pure/Isar/proof_context.ML	Mon Jun 08 00:25:10 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Jun 08 18:56:04 2015 +0100
@@ -105,27 +105,27 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val norm_export_morphism: Proof.context -> Proof.context -> morphism
-  val bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
+  val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
+  val bind_terms: (indexname * term) list -> Proof.context -> Proof.context
+  val export_bind_terms: (indexname * term) list -> Proof.context -> 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 -> (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 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 ->
     (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: (term * term list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   val bind_propp_cmd: (string * string list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   val bind_propp_schematic: (term * term list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   val bind_propp_schematic_cmd: (string * string list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   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
@@ -257,10 +257,7 @@
     (mode, f syntax, tsig, consts, facts, cases));
 
 fun map_syntax_idents f ctxt =
-  let
-    val idents = Syntax_Trans.get_idents ctxt;
-    val (opt_idents', syntax') = f (#syntax (rep_data ctxt));
-  in
+  let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in
     ctxt
     |> map_syntax (K syntax')
     |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents')
@@ -832,17 +829,23 @@
 
 (* bind_terms *)
 
-val bind_terms = fold (fn (xi, t) => fn ctxt =>
+val maybe_bind_terms = fold (fn (xi, t) => fn ctxt =>
   ctxt
   |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
 
+val bind_terms = maybe_bind_terms o map (apsnd SOME);
+
+fun export_bind_terms binds ctxt ctxt0 =
+  let val ts0 = map Term.close_schematic_term (Variable.export_terms ctxt ctxt0 (map snd binds))
+  in bind_terms (map fst binds ~~ ts0) ctxt0 end;
+
 
 (* auto_bind *)
 
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
-fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f ctxt ts));
+fun auto_bind f ts ctxt = ctxt |> maybe_bind_terms (map drop_schematic (f ctxt ts));
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
@@ -867,12 +870,11 @@
     val binds' =
       if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds)
       else binds;
-    val binds'' = map (apsnd SOME) binds';
     val ctxt'' =
       tap (Variable.warn_extra_tfrees ctxt)
        (if gen then
-          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds''
-        else ctxt' |> bind_terms binds'');
+          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds'
+        else ctxt' |> bind_terms binds');
   in (ts, ctxt'') end;
 
 in
@@ -890,33 +892,25 @@
 
 local
 
-fun prep_propp mode prep_props args context =
+fun prep_propp mode prep_props raw_args ctxt =
   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 (propp, context') end;
+    val props = prep_props (set_mode mode ctxt) (maps (map fst) raw_args);
+    val ctxt' = fold Variable.declare_term props ctxt;
+    val patss = maps (map (prep_props (set_mode mode_pattern ctxt') o snd)) raw_args;
+    val propp = unflat raw_args (props ~~ patss);
+  in (propp, ctxt') end;
 
 fun gen_bind_propp mode parse_prop raw_args ctxt =
   let
     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;
-    fun gen_binds ctxt0 = ctxt0
-      |> bind_terms (map #1 binds ~~
-          map (SOME o Term.close_schematic_term) (Variable.export_terms ctxt' ctxt0 (map #2 binds)));
-  in ((propss, gen_binds), ctxt' |> bind_terms (map (apsnd SOME) binds)) end;
+    val propss = map (map fst) args;
+    val binds = (maps o maps) (simult_matches ctxt') args;
+  in ((propss, binds), bind_terms binds ctxt') end;
 
 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_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 (map o cert_prop);
 val bind_propp_cmd = gen_bind_propp mode_default Syntax.read_props;
@@ -1242,7 +1236,7 @@
     val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
-    |> bind_terms (map drop_schematic binds)
+    |> maybe_bind_terms (map drop_schematic binds)
     |> update_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;