1.1 --- a/etc/isar-keywords.el	Thu May 22 15:31:36 2014 +0200
     1.2 +++ b/etc/isar-keywords.el	Thu May 22 15:49:36 2014 +0200
     1.3 @@ -149,9 +149,11 @@
     1.4      "no_translations"
     1.5      "no_type_notation"
     1.6      "nominal_datatype"
     1.7 +    "nominal_function"
     1.8      "nominal_inductive"
     1.9      "nominal_inductive2"
    1.10      "nominal_primrec"
    1.11 +    "nominal_termination"
    1.12      "nonterminal"
    1.13      "notation"
    1.14      "note"
    1.15 @@ -315,6 +317,7 @@
    1.16      "avoids"
    1.17      "begin"
    1.18      "binder"
    1.19 +    "binds"
    1.20      "checking"
    1.21      "class_instance"
    1.22      "class_relation"
    1.23 @@ -613,9 +616,11 @@
    1.24      "interpretation"
    1.25      "lemma"
    1.26      "lift_definition"
    1.27 +    "nominal_function"
    1.28      "nominal_inductive"
    1.29      "nominal_inductive2"
    1.30      "nominal_primrec"
    1.31 +    "nominal_termination"
    1.32      "pcpodef"
    1.33      "permanent_interpretation"
    1.34      "primcorecursive"

     2.1 --- a/src/HOL/ROOT	Thu May 22 15:31:36 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Thu May 22 15:49:36 2014 +0200
     2.3 @@ -582,6 +582,7 @@
     2.4      ML
     2.5      SAT_Examples
     2.6      Sudoku
     2.7 +    Nominal2_Dummy
     2.8    theories [skip_proofs = false]
     2.9      Meson_Test
    2.10    theories [condition = SVC_HOME]

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Nominal2_Dummy.thy	Thu May 22 15:49:36 2014 +0200
     3.3 @@ -0,0 +1,22 @@
     3.4 +header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close>  (* Proof General legacy *)
     3.5 +
     3.6 +theory Nominal2_Dummy
     3.7 +imports Main
     3.8 +keywords
     3.9 +  "nominal_datatype" :: thy_decl and
    3.10 +  "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
    3.11 +  "atom_decl" "equivariance" :: thy_decl and
    3.12 +  "avoids" "binds"
    3.13 +begin
    3.14 +
    3.15 +ML \<open>
    3.16 +Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
    3.17 +Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
    3.18 +Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
    3.19 +Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
    3.20 +Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
    3.21 +Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
    3.22 +\<close>
    3.23 +
    3.24 +end
    3.25 +