# HG changeset patch
# User wenzelm
# Date 1438007712 -7200
# Node ID 57dd0b45fc2135f05dfef48974daa47e0d4fc6bf
# Parent  9a9694087cdafb85bb645b4000f7dbdb5714ab5b
tuned signature for print_nested_cases;

diff -r 9a9694087cda -r 57dd0b45fc21 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jul 27 15:13:05 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jul 27 16:35:12 2015 +0200
@@ -139,6 +139,7 @@
   val add_assms_cmd: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
+  val dest_cases: Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
   val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context