# HG changeset patch
# User wenzelm
# Date 1138059808 -3600
# Node ID 932750b85c5bd95d30ee26fe2b99007471df83c8
# Parent  97911ffe9222a2388f13878c62fe383f28df7cce
axiomatization: optional vars;

diff -r 97911ffe9222 -r 932750b85c5b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 24 00:43:27 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 24 00:43:28 2006 +0100
@@ -195,8 +195,10 @@
 
 val axiomatizationP =
   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
-    (P.fixes -- Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) []
-    >> (Toplevel.theory o (#2 oo Specification.axiomatize)));
+    (P.opt_locale_target --
+      Scan.optional P.fixes [] --
+      Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) []
+    >> (fn ((x, y), z) => Toplevel.theory_context (#2 o Specification.axiomatization x y z)));
 
 
 (* theorems *)