# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1332242770 0
# Node ID 92b9b8d2888d6333fe3a866c6c12d382b6199157
# Parent  301b74fcd6148b6d7ebf6f71f97c370eded6efdb
updated to new Isabelle (20 March)

diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/Nominal2.thy	Tue Mar 20 11:26:10 2012 +0000
@@ -710,8 +710,6 @@
   fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
 in
 
-val _ = Keyword.keyword "binds"
-
 val opt_name = Scan.option (P.binding --| Args.colon)
 
 val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ
@@ -742,8 +740,9 @@
 end
 
 (* Command Keyword *)
-val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
-  (main_parser >> nominal_datatype2_cmd)
+val _ = Outer_Syntax.local_theory ("nominal_datatype", Keyword.thy_decl) 
+  "declaration of nominal datatypes" 
+    (main_parser >> nominal_datatype2_cmd)
 *}
 
 
diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_atoms.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -76,14 +76,10 @@
   end;
 
 (** outer syntax **)
-
-local structure P = Parse and K = Keyword in
-
 val _ =
-  Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
-    ((P.binding -- Scan.option (Args.parens (P.binding))) >>
-      (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
+  Outer_Syntax.command ("atom_decl", Keyword.thy_decl) 
+    "declaration of a concrete atom type" 
+      ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
+        (Toplevel.print oo (Toplevel.theory o add_atom_decl)))
 
 end;
-
-end;
diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_eqvt.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -124,13 +124,11 @@
     fold_map note_named_thm (names ~~ thms) ctxt |> snd
   end
 
-local structure P = Parse and K = Keyword in
 
 val _ =
-  Outer_Syntax.local_theory "equivariance"
+  Outer_Syntax.local_theory ("equivariance", Keyword.thy_decl)
     "Proves equivariance for inductive predicate involving nominal datatypes." 
-      K.thy_decl (P.xname >> equivariance_cmd);
+      (Parse.xname >> equivariance_cmd)
 
-end;
 
 end (* structure *)
diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_function.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -275,10 +275,10 @@
 
 (* nominal *)
 val _ =
-  Outer_Syntax.local_theory_to_proof' "nominal_primrec" "define general recursive nominal functions"
-  Keyword.thy_goal
-  (nominal_function_parser nominal_default_config
-     >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
+  Outer_Syntax.local_theory_to_proof' ("nominal_primrec", Keyword.thy_goal) 
+    "define general recursive nominal functions"
+       (nominal_function_parser nominal_default_config
+          >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
 
 
 end
diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_inductive.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -420,23 +420,19 @@
 
 (* outer syntax *)
 local
-  structure P = Parse;
-  structure S = Scan
-  
-  val _ = Keyword.keyword "avoids"
 
   val single_avoid_parser = 
-    P.name -- (P.$$$ ":" |-- P.and_list1 P.term)
+    Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term)
 
   val avoids_parser = 
-    S.optional (P.$$$ "avoids" |-- P.enum1 "|" single_avoid_parser) []
+    Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) []
 
-  val main_parser = P.xname -- avoids_parser
+  val main_parser = Parse.xname -- avoids_parser
 in
   val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_inductive"
-    "prove strong induction theorem for inductive predicate involving nominal datatypes"
-      Keyword.thy_goal (main_parser >> prove_strong_inductive_cmd)
+    Outer_Syntax.local_theory_to_proof ("nominal_inductive", Keyword.thy_goal)
+      "prove strong induction theorem for inductive predicate involving nominal datatypes"
+        (main_parser >> prove_strong_inductive_cmd)
 end
 
 end
diff -r 301b74fcd614 -r 92b9b8d2888d Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/nominal_termination.ML	Tue Mar 20 11:26:10 2012 +0000
@@ -101,15 +101,15 @@
 (* outer syntax *)
 
 val option_parser =
-  (Scan.optional (Parse.$$$ "(" |-- Parse.!!! 
+  (Scan.optional (@{keyword "("} |-- Parse.!!! 
     ((Parse.reserved "eqvt" >> K (true, true)) ||
-     (Parse.reserved "no_eqvt" >> K (true, false))) --| Parse.$$$ ")") (false, false))
+     (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
-  Keyword.thy_goal
-  (option_parser -- Scan.option Parse.term >> 
-     (fn ((is_nominal, is_eqvt), opt_trm) => 
-        if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))
+  Outer_Syntax.local_theory_to_proof ("termination", Keyword.thy_goal) 
+    "prove termination of a recursive function"
+      (option_parser -- Scan.option Parse.term >> 
+        (fn ((is_nominal, is_eqvt), opt_trm) => 
+           if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))
 
 end