--- a/src/Pure/Isar/parse_spec.ML Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML Wed Jun 10 14:46:31 2015 +0200
@@ -24,6 +24,7 @@
val locale_expression: bool -> Expression.expression parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
+ val if_prems: (Attrib.binding * (string * string list) list) list parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
end;
@@ -131,6 +132,8 @@
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
+val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
+
val obtain_case =
Parse.parbinding --
(Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --