--- a/src/Pure/Pure.thy Sat May 28 17:35:12 2016 +0200
+++ b/src/Pure/Pure.thy Sat May 28 21:38:58 2016 +0200
@@ -351,11 +351,15 @@
(Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
>> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
+val axiomatization =
+ Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --
+ Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
+
val _ =
Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
(Scan.optional Parse.fixes [] --
- Scan.optional (Parse.where_ |-- Parse.!!! Parse_Spec.specification) ([], [])
- >> (fn (a, (b, c)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c)));
+ Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
+ >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
in end\<close>