# HG changeset patch
# User webertj
# Date 1343997985 -7200
# Node ID 87d1e815aa59ac810c8d186078cc678568a3a89d
# Parent  14c7d7e29c4454c2a38930990d33108e622f55cc
command_spec antiquotation.

diff -r 14c7d7e29c44 -r 87d1e815aa59 Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_atoms.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -77,7 +77,7 @@
 
 (** outer syntax **)
 val _ =
-  Outer_Syntax.command ("atom_decl", Keyword.thy_decl) 
+  Outer_Syntax.command @{command_spec "atom_decl"}
     "declaration of a concrete atom type" 
       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
         (Toplevel.print oo (Toplevel.theory o add_atom_decl)))
diff -r 14c7d7e29c44 -r 87d1e815aa59 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_eqvt.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -126,7 +126,7 @@
 
 
 val _ =
-  Outer_Syntax.local_theory ("equivariance", Keyword.thy_decl)
+  Outer_Syntax.local_theory @{command_spec "equivariance"}
     "Proves equivariance for inductive predicate involving nominal datatypes." 
       (Parse.xname >> equivariance_cmd)
 
diff -r 14c7d7e29c44 -r 87d1e815aa59 Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_termination.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -106,7 +106,7 @@
      (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof ("termination", Keyword.thy_goal) 
+  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
     "prove termination of a recursive function"
       (option_parser -- Scan.option Parse.term >> 
         (fn ((is_nominal, is_eqvt), opt_trm) =>