# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1324141045 0
# Node ID f89ee40fbb082eeb88652dd2f2ac41faacbfe000
# Parent  c32bdb3f0a68c95e16cef5407c4d786dfd8ddd94
backported no_eqvt changeset 1afcbaf4242b

diff -r c32bdb3f0a68 -r f89ee40fbb08 Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Sat Dec 17 16:36:51 2011 +0000
+++ b/Nominal/nominal_termination.ML	Sat Dec 17 16:57:25 2011 +0000
@@ -10,10 +10,9 @@
 signature NOMINAL_FUNCTION_TERMINATION =
 sig
   include NOMINAL_FUNCTION_DATA
-
-  val termination : term option -> local_theory -> Proof.state
-  val termination_cmd : string option -> local_theory -> Proof.state
-
+  
+  val termination : bool -> term option -> local_theory -> Proof.state
+  val termination_cmd : bool -> string option -> local_theory -> Proof.state
 end
 
 structure Nominal_Function_Termination : NOMINAL_FUNCTION_TERMINATION =
@@ -30,7 +29,7 @@
 
 val eqvt_attrib =  Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 
-fun prepare_termination_proof prep_term raw_term_opt lthy =
+fun prepare_termination_proof prep_term is_eqvt raw_term_opt lthy =
   let
     val term_opt = Option.map (prep_term lthy) raw_term_opt
     val info = the (case term_opt of
@@ -59,7 +58,7 @@
         in
           lthy
           |> add_simps I "simps" I simp_attribs tsimps
-          ||>> Local_Theory.note ((qualify "eqvt", [eqvt_attrib]), teqvts)
+          ||>> Local_Theory.note ((qualify "eqvt", if is_eqvt then [eqvt_attrib] else []), teqvts)
           ||>> Local_Theory.note
              ((qualify "induct",
                [Attrib.internal (K (Rule_Cases.case_names case_names))]),
@@ -79,9 +78,9 @@
     (goal, afterqed, termination)
   end
 
-fun gen_termination prep_term raw_term_opt lthy =
+fun gen_termination prep_term is_eqvt raw_term_opt lthy =
   let
-    val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
+    val (goal, afterqed, termination) = prepare_termination_proof prep_term is_eqvt raw_term_opt lthy
   in
     lthy
     |> Proof_Context.note_thmss ""
@@ -101,13 +100,14 @@
 
 val option_parser =
   (Scan.optional (Parse.$$$ "(" |-- Parse.!!! 
-    (Parse.reserved "eqvt" >> K true) --| Parse.$$$ ")") false)
+    ((Parse.reserved "eqvt" >> K (true, true)) ||
+     (Parse.reserved "no_eqvt" >> K (true, false))) --| Parse.$$$ ")") (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_eqvt, trm) => 
-        if is_eqvt then termination_cmd trm else Function.termination_cmd trm))
+    (fn ((is_nominal, is_eqvt), opt_trm) => 
+       if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))
 
 end