--- a/Nominal/Ex/AuxNoFCB.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/AuxNoFCB.thy	Mon May 19 16:45:46 2014 +0100
@@ -15,7 +15,7 @@
   apply (rule, perm_simp, rule, rule)
   by pat_completeness auto
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function lam2_rec where
   "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs"
@@ -74,7 +74,7 @@
   apply simp
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma lam_rec2_cong[fundef_cong]:
   "(\<And>s1 s2 s3 s4. l = App s1 s2 \<Longrightarrow> l2 = App s3 s4  \<Longrightarrow> faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \<Longrightarrow>
@@ -106,7 +106,7 @@
   apply (rule, perm_simp, rule, rule)
   by pat_completeness auto
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all
 
 lemma aux_simps[simp]:
@@ -233,7 +233,7 @@
   apply (simp add: flip_fresh_fresh flip_eqvt)
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs"
   apply (induct xs)

--- a/Nominal/Ex/Beta.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/Beta.thy	Mon May 19 16:45:46 2014 +0100
@@ -34,7 +34,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma forget:

--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 16:45:46 2014 +0100
@@ -63,7 +63,7 @@
 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
 
@@ -89,7 +89,7 @@
   apply (simp add: Abs1_eq_iff CPS.eqvt)
   by blast
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure size") (simp_all)
 
 lemma convert_supp[simp]:
@@ -143,7 +143,7 @@
 apply(simp_all add: flip_fresh_fresh)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
 
 section{* lemma related to Kapply *}

--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon May 19 16:45:46 2014 +0100
@@ -32,7 +32,7 @@
   apply (simp add: flip_fresh_fresh)
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function
   ccomp :: "cpsctxt => cpsctxt => cpsctxt"
@@ -57,7 +57,7 @@
   apply (simp add: flip_fresh_fresh)
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function
     CPSv :: "lt => lt"

--- a/Nominal/Ex/CPS/Lt.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Mon May 19 16:45:46 2014 +0100
@@ -33,7 +33,7 @@
   apply(simp add: perm_supp_eq fresh_star_Pair)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
   shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M"
@@ -54,7 +54,7 @@
   by (auto)
      (erule lt.exhaust, auto)
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure size") (simp_all)
 
 inductive

--- a/Nominal/Ex/CR.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/CR.thy	Mon May 19 16:45:46 2014 +0100
@@ -30,7 +30,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma forget:

--- a/Nominal/Ex/Classical.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/Classical.thy	Mon May 19 16:45:46 2014 +0100
@@ -249,7 +249,7 @@
   apply(blast)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 nominal_function 
@@ -443,7 +443,7 @@
   apply(blast)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 thm crename.eqvt nrename.eqvt

--- a/Nominal/Ex/Lambda.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon May 19 16:45:46 2014 +0100
@@ -86,7 +86,7 @@
 apply(all_trivials)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 thm is_app_def
 thm is_app.eqvt
@@ -106,7 +106,7 @@
 apply(simp_all)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function 
   rand :: "lam \<Rightarrow> lam option"
@@ -121,7 +121,7 @@
 apply(simp_all)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function 
   is_eta_nf :: "lam \<Rightarrow> bool"
@@ -142,7 +142,7 @@
 apply(simp add: eqvt_at_def conj_eqvt)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_datatype path = Left | Right | In
 
@@ -181,7 +181,7 @@
 apply(simp add: perm_supp_eq)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma var_pos1:
   assumes "atom y \<notin> supp t"
@@ -227,7 +227,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 
 section {* free name function *}
@@ -252,7 +252,7 @@
 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 text {* a small test lemma *}
 lemma shows "supp t = set (frees_lst t)"
@@ -280,7 +280,7 @@
   apply(simp add: Diff_eqvt eqvt_at_def)
   done
 
-termination (eqvt) 
+nominal_termination (eqvt) 
   by lexicographic_order
 
 lemma "frees_set t = supp t"
@@ -303,7 +303,7 @@
   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
   
 thm height.simps
@@ -338,7 +338,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 thm subst.eqvt
@@ -530,7 +530,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 
@@ -557,7 +557,7 @@
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 
@@ -591,7 +591,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 section {* De Bruijn Terms *}
@@ -649,7 +649,7 @@
   apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma transdb_eqvt[eqvt]:
@@ -722,7 +722,7 @@
 
 
 (* a small test
-termination (eqvt) sorry
+nominal_termination (eqvt) sorry
 
 lemma 
   assumes "x \<noteq> y"
@@ -774,7 +774,7 @@
   apply (simp add: eqvt_def permute_fun_app_eq)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 

--- a/Nominal/Ex/LetRec.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/LetRec.thy	Mon May 19 16:45:46 2014 +0100
@@ -61,7 +61,7 @@
   apply(simp add: eqvt_at_def)
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 thm height_trm_height_bp.eqvt
 

--- a/Nominal/Ex/LetRecFunNo.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/LetRecFunNo.thy	Mon May 19 16:45:46 2014 +0100
@@ -53,7 +53,7 @@
   apply clarify
   apply metis
   done
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
   "substarec fac ANil = ANil"
@@ -64,7 +64,7 @@
   apply (rule_tac y="b" in trm_assn.exhaust(2))
   apply auto
   done
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma [fundef_cong]:
  "(\<And>t1 t2. t = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow>

--- a/Nominal/Ex/Local_Contexts.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/Local_Contexts.thy	Mon May 19 16:45:46 2014 +0100
@@ -55,7 +55,7 @@
 apply (metis Pair_eqvt perm_supp_eq)
 done
 
-termination (in name_subst) (eqvt) by lexicographic_order
+nominal_termination (in name_subst) (eqvt) by lexicographic_order
 
 inductive (in name_subst) beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<longrightarrow>\<^sub>\<beta>" 90)
 where

--- a/Nominal/Ex/Pi.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/Pi.thy	Mon May 19 16:45:46 2014 +0100
@@ -38,7 +38,7 @@
   apply(rule_tac y="b" in list.exhaust)
   by(auto)
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (lexicographic_order)
 
 
@@ -379,7 +379,7 @@
   apply(simp)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (lexicographic_order)
 
 lemma forget_mix:

--- a/Nominal/Ex/SFT/Consts.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/SFT/Consts.thy	Mon May 19 16:45:46 2014 +0100
@@ -99,7 +99,7 @@
     by (rule, perm_simp, rule)
 qed
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma supp_numeral[simp]:
   "supp \<lbrace>x\<rbrace> = supp x"
@@ -144,7 +144,7 @@
   apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma ltgt_eq_iff[simp]:
   "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"

--- a/Nominal/Ex/SFT/LambdaTerms.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/SFT/LambdaTerms.thy	Mon May 19 16:45:46 2014 +0100
@@ -52,7 +52,7 @@
     by (rule, perm_simp, rule)
 qed
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

--- a/Nominal/Ex/SubstNoFcb.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/SubstNoFcb.thy	Mon May 19 16:45:46 2014 +0100
@@ -31,7 +31,7 @@
   apply (metis (no_types) Pair_inject lam.distinct)+
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma lam_rec_cong[fundef_cong]:
   " (\<And>v. l = Var v \<Longrightarrow> fv v = fv' v) \<Longrightarrow>
@@ -58,7 +58,7 @@
 apply (rule, perm_simp, rule, rule)
 by pat_completeness auto
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma fresh_fun_eqvt_app3:
   assumes e: "eqvt f"

--- a/Nominal/Ex/TypeSchemes1.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Mon May 19 16:45:46 2014 +0100
@@ -89,7 +89,7 @@
   apply(simp_all)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma subst_id1:
@@ -161,7 +161,7 @@
   apply blast
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (lexicographic_order)
 
 
@@ -301,7 +301,7 @@
 apply(simp)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
   
 lemma better:
@@ -412,7 +412,7 @@
   apply(simp_all)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma tt:

--- a/Nominal/Ex/TypeSchemes2.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy	Mon May 19 16:45:46 2014 +0100
@@ -155,7 +155,7 @@
   done
 
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 text {* Some Tests about Alpha-Equality *}
 

--- a/Nominal/Nominal2.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Nominal2.thy	Mon May 19 16:45:46 2014 +0100
@@ -3,7 +3,7 @@
   Nominal2_Base Nominal2_Abs Nominal2_FCB
 keywords
   "nominal_datatype" :: thy_decl and
-  "nominal_function" "nominal_inductive" :: thy_goal and
+  "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
   "avoids" "binds"
 begin
 

--- a/Nominal/nominal_termination.ML	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/nominal_termination.ML	Mon May 19 16:45:46 2014 +0100
@@ -103,14 +103,13 @@
 
 val option_parser =
   (Scan.optional (@{keyword "("} |-- Parse.!!! 
-    ((Parse.reserved "eqvt" >> K (true, true)) ||
-     (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))
+    ((Parse.reserved "eqvt" >> K true) ||
+     (Parse.reserved "no_eqvt" >> K false)) --| @{keyword ")"}) (false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
-    "prove termination of a recursive function"
+  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_termination"}
+    "prove termination of a recursive nominal 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))
+        (fn (is_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm))
 
 end

--- a/Tutorial/Lambda.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Tutorial/Lambda.thy	Mon May 19 16:45:46 2014 +0100
@@ -47,7 +47,7 @@
 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
   
 
@@ -76,7 +76,7 @@
   apply(simp add: perm_supp_eq fresh_star_Pair)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_fact: