# HG changeset patch
# User wenzelm
# Date 952534603 -3600
# Node ID 7313627803f463d69a566f86750a4bef3367645b
# Parent  6b45749d37d685d250a9997925a64b28c7439378
added invoke_case;

diff -r 6b45749d37d6 -r 7313627803f4 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Mar 08 17:55:17 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 08 17:56:43 2000 +0100
@@ -79,6 +79,7 @@
   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 invoke_case: string * Comment.text -> ProofHistory.T -> ProofHistory.T
   val theorem: (bstring * Args.src list * (string * (string list * string list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
   val theorem_i: (bstring * theory attribute list * (term * (term list * term list)))
@@ -287,6 +288,7 @@
 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 invoke_case = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
 
 
 (* statements *)