1.1 --- a/src/Pure/Isar/proof.ML	Sun Apr 25 15:52:03 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Apr 25 16:10:05 2010 +0200
     1.3 @@ -41,8 +41,6 @@
     1.4    val raw_goal: state -> {context: context, facts: thm list, goal: thm}
     1.5    val goal: state -> {context: context, facts: thm list, goal: thm}
     1.6    val simple_goal: state -> {context: context, goal: thm}
     1.7 -  val match_bind: (term list * term) list -> state -> state
     1.8 -  val match_bind_cmd: (string list * string) list -> state -> state
     1.9    val let_bind: (term list * term) list -> state -> state
    1.10    val let_bind_cmd: (string list * string) list -> state -> state
    1.11    val fix: (binding * typ option * mixfix) list -> state -> state
    1.12 @@ -523,22 +521,20 @@
    1.13  
    1.14  (** context elements **)
    1.15  
    1.16 -(* bindings *)
    1.17 +(* let bindings *)
    1.18  
    1.19  local
    1.20  
    1.21  fun gen_bind bind args state =
    1.22    state
    1.23    |> assert_forward
    1.24 -  |> map_context (bind args #> snd)
    1.25 +  |> map_context (bind true args #> snd)
    1.26    |> put_facts NONE;
    1.27  
    1.28  in
    1.29  
    1.30 -val match_bind = gen_bind (ProofContext.match_bind_i false);
    1.31 -val match_bind_cmd = gen_bind (ProofContext.match_bind false);
    1.32 -val let_bind = gen_bind (ProofContext.match_bind_i true);
    1.33 -val let_bind_cmd = gen_bind (ProofContext.match_bind true);
    1.34 +val let_bind = gen_bind ProofContext.match_bind_i;
    1.35 +val let_bind_cmd = gen_bind ProofContext.match_bind;
    1.36  
    1.37  end;
    1.38