--- a/src/Pure/Pure.thy Tue Apr 26 21:46:12 2016 +0200
+++ b/src/Pure/Pure.thy Tue Apr 26 22:39:17 2016 +0200
@@ -758,8 +758,8 @@
val _ =
Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
- (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
- >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
+ (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
+ >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
val _ =
Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"