# HG changeset patch
# User wenzelm
# Date 1400766576 -7200
# Node ID 8a1be5efe628dabad8d7ef41d8fef67327621a16
# Parent  0ee2d5b566f64ded8f6057269913b9a92d42ee22
include Nominal2 keywords -- Proof General legacy;

diff -r 0ee2d5b566f6 -r 8a1be5efe628 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu May 22 15:31:36 2014 +0200
+++ b/etc/isar-keywords.el	Thu May 22 15:49:36 2014 +0200
@@ -149,9 +149,11 @@
     "no_translations"
     "no_type_notation"
     "nominal_datatype"
+    "nominal_function"
     "nominal_inductive"
     "nominal_inductive2"
     "nominal_primrec"
+    "nominal_termination"
     "nonterminal"
     "notation"
     "note"
@@ -315,6 +317,7 @@
     "avoids"
     "begin"
     "binder"
+    "binds"
     "checking"
     "class_instance"
     "class_relation"
@@ -613,9 +616,11 @@
     "interpretation"
     "lemma"
     "lift_definition"
+    "nominal_function"
     "nominal_inductive"
     "nominal_inductive2"
     "nominal_primrec"
+    "nominal_termination"
     "pcpodef"
     "permanent_interpretation"
     "primcorecursive"
diff -r 0ee2d5b566f6 -r 8a1be5efe628 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu May 22 15:31:36 2014 +0200
+++ b/src/HOL/ROOT	Thu May 22 15:49:36 2014 +0200
@@ -582,6 +582,7 @@
     ML
     SAT_Examples
     Sudoku
+    Nominal2_Dummy
   theories [skip_proofs = false]
     Meson_Test
   theories [condition = SVC_HOME]
diff -r 0ee2d5b566f6 -r 8a1be5efe628 src/HOL/ex/Nominal2_Dummy.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Nominal2_Dummy.thy	Thu May 22 15:49:36 2014 +0200
@@ -0,0 +1,22 @@
+header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close>  (* Proof General legacy *)
+
+theory Nominal2_Dummy
+imports Main
+keywords
+  "nominal_datatype" :: thy_decl and
+  "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
+  "atom_decl" "equivariance" :: thy_decl and
+  "avoids" "binds"
+begin
+
+ML \<open>
+Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
+Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
+\<close>
+
+end
+