# HG changeset patch
# User wenzelm
# Date 1468620663 -7200
# Node ID 1c7b1e294fb5fd47494b99aac6efef8366b65a6f
# Parent  1c2c045decb361b6b4dd98ca49d1b5c25fe22c6c
tuned signature;

diff -r 1c2c045decb3 -r 1c7b1e294fb5 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Fri Jul 15 23:47:07 2016 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Sat Jul 16 00:11:03 2016 +0200
@@ -12,7 +12,9 @@
     binds: (indexname * term option) list,
     cases: (string * T) list}
   type cases = (string * T option) list
+  val case_conclN: string
   val case_hypsN: string
+  val case_premsN: string
   val strip_params: term -> (string * typ) list
   type info = ((string * string list) * string list) list
   val make_common: Proof.context -> term -> info -> cases