--- a/src/Pure/Isar/proof_context.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Feb 02 11:38:38 2010 +0100
@@ -33,6 +33,7 @@
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
val facts_of: Proof.context -> Facts.T
+ val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
val transfer_syntax: theory -> Proof.context -> Proof.context
val transfer: theory -> Proof.context -> Proof.context
val theory: (theory -> theory) -> Proof.context -> Proof.context