# HG changeset patch
# User wenzelm
# Date 1568730417 -7200
# Node ID cb63a978a52e2b031ad187ae71a5fd579c31e53c
# Parent  99e24569cc1f3ac0ef00a04dc5539c179d8724dc
clarified signature -- removed unused option (see acb0807ddb56);

diff -r 99e24569cc1f -r cb63a978a52e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Sep 16 23:51:24 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 17 16:26:57 2019 +0200
@@ -560,7 +560,7 @@
 fun gen_bind bind args state =
   state
   |> assert_forward
-  |> map_context (bind true args #> snd)
+  |> map_context (bind args #> snd)
   |> reset_facts;
 
 in
diff -r 99e24569cc1f -r cb63a978a52e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 16 23:51:24 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 17 16:26:57 2019 +0200
@@ -108,10 +108,8 @@
   val norm_export_morphism: Proof.context -> Proof.context -> morphism
   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: (term list * term) list -> Proof.context -> term list * Proof.context
+  val match_bind_cmd: (string list * string) list -> Proof.context -> 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 ->
@@ -878,7 +876,7 @@
 
 local
 
-fun gen_bind prep_terms gen raw_binds ctxt =
+fun gen_bind prep_terms raw_binds ctxt =
   let
     fun prep_bind (raw_pats, t) ctxt1 =
       let
@@ -890,23 +888,20 @@
 
     val ts = prep_terms ctxt dummyT (map snd raw_binds);
     val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt);
-    val binds' =
-      if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds)
-      else binds;
+    val binds' = map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds);
+
     val ctxt'' =
-      tap (Variable.warn_extra_tfrees ctxt)
-       (if gen then
-          ctxt (*sic!*)
-          |> fold Variable.declare_term (map #2 binds')
-          |> fold cert_bind_term binds'
-        else ctxt' |> fold cert_bind_term binds');
+      ctxt
+      |> fold Variable.declare_term (map #2 binds')
+      |> fold cert_bind_term binds';
+    val _ = Variable.warn_extra_tfrees ctxt ctxt'';
   in (ts, ctxt'') end;
 
-in
-
 fun read_terms ctxt T =
   map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
 
+in
+
 val match_bind = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
 val match_bind_cmd = gen_bind read_terms;