# HG changeset patch
# User wenzelm
# Date 954419135 -7200
# Node ID 419166fa66d0d56e080dbe8aca504fff448705b0
# Parent  30cc975727f16f67b736772ad3b5071b12bacec7
let_bind(_i): polymorphic version;

diff -r 30cc975727f1 -r 419166fa66d0 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 30 14:24:46 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 30 14:25:35 2000 +0200
@@ -333,7 +333,7 @@
 val letP =
   OuterSyntax.command "let" "bind text variables" K.prf_decl
     (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
-      >> (Toplevel.print oo (Toplevel.proof o IsarThy.match_bind)));
+      >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
 
 val caseP =
   OuterSyntax.command "case" "invoke local context" K.prf_asm
diff -r 30cc975727f1 -r 419166fa66d0 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Mar 30 14:24:46 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 30 14:25:35 2000 +0200
@@ -76,8 +76,8 @@
   val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
   val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
-  val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
-  val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val let_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val let_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T
   val invoke_case_i: (string * Proof.context attribute list) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
@@ -288,8 +288,8 @@
 
 val fix = ProofHistory.apply o Proof.fix o map Comment.ignore;
 val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore;
-val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore;
-val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore;
+val let_bind = ProofHistory.apply o Proof.let_bind o map Comment.ignore;
+val let_bind_i = ProofHistory.apply o Proof.let_bind_i o map Comment.ignore;
 
 fun invoke_case ((name, src), comment_ignore) = ProofHistory.apply (fn state =>
   Proof.invoke_case (name, map (Attrib.local_attribute (Proof.theory_of state)) src) state);