# HG changeset patch
# User wenzelm
# Date 1139255989 -3600
# Node ID 5e5950ac714586974cb02a8abe758aeaad989037
# Parent  b6b19cc8454fa401da81a2558516bb77676abeca
Toplevel.local_theory;

diff -r b6b19cc8454f -r 5e5950ac7145 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Feb 06 20:59:48 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Feb 06 20:59:49 2006 +0100
@@ -193,7 +193,7 @@
 val definitionP =
   OuterSyntax.command "definition" "standard constant definition" K.thy_decl
     (P.opt_locale_target -- Scan.repeat1 constdef
-    >> (fn (x, y) => Toplevel.theory_context (#2 o Specification.definition x y)));
+    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
 
 
 (* constant specifications *)
@@ -201,9 +201,9 @@
 val axiomatizationP =
   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
     (P.opt_locale_target --
-      Scan.optional P.fixes [] --
-      Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.spec)) []
-    >> (fn ((x, y), z) => Toplevel.theory_context (#2 o Specification.axiomatization x y z)));
+     (Scan.optional P.fixes [] --
+      Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.spec)) [])
+    >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
 
 
 (* theorems *)