# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID 0b8871677e0b83b45367964bd46a32aad2e2993a
# Parent  136fe16e726af658dd28bf412efe79c4368e09cb
use same name for feature internally as in user interface, to facilitate grepping

diff -r 136fe16e726a -r 0b8871677e0b src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -496,7 +496,7 @@
   Disc of coeqn_data_disc |
   Sel of coeqn_data_sel;
 
-fun dissect_coeqn_disc seq fun_names (basic_ctr_specss : basic_corec_ctr_spec list list)
+fun dissect_coeqn_disc sequential fun_names (basic_ctr_specss : basic_corec_ctr_spec list list)
     maybe_ctr_rhs maybe_code_rhs prems' concl matchedsss =
   let
     fun find_subterm p =
@@ -532,11 +532,11 @@
     val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
     val prems = map (abstract (List.rev fun_args)) prems';
     val real_prems =
-      (if catch_all orelse seq then maps s_not_conj matchedss else []) @
+      (if catch_all orelse sequential then maps s_not_conj matchedss else []) @
       (if catch_all then [] else prems);
 
     val matchedsss' = AList.delete (op =) fun_name matchedsss
-      |> cons (fun_name, if seq then matchedss @ [prems] else matchedss @ [real_prems]);
+      |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [real_prems]);
 
     val user_eqn =
       (real_prems, concl)
@@ -591,7 +591,7 @@
     }
   end;
 
-fun dissect_coeqn_ctr seq fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn'
+fun dissect_coeqn_ctr sequential fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn'
     maybe_code_rhs prems concl matchedsss =
   let
     val (lhs, rhs) = HOLogic.dest_eq concl;
@@ -604,7 +604,7 @@
     val disc_concl = betapply (disc, lhs);
     val (maybe_eqn_data_disc, matchedsss') = if length basic_ctr_specs = 1
       then (NONE, matchedsss)
-      else apfst SOME (dissect_coeqn_disc seq fun_names basic_ctr_specss
+      else apfst SOME (dissect_coeqn_disc sequential fun_names basic_ctr_specss
           (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs prems disc_concl matchedsss);
 
     val sel_concls = sels ~~ ctr_args
@@ -650,8 +650,8 @@
       ctr_premss ctr_concls matchedsss
   end;
 
-fun dissect_coeqn lthy seq has_call fun_names (basic_ctr_specss : basic_corec_ctr_spec list list)
-    eqn' maybe_of_spec matchedsss =
+fun dissect_coeqn lthy sequential has_call fun_names
+    (basic_ctr_specss : basic_corec_ctr_spec list list) eqn' maybe_of_spec matchedsss =
   let
     val eqn = drop_All eqn'
       handle TERM _ => primcorec_error_eqn "malformed function equation" eqn';
@@ -671,13 +671,14 @@
     if member (op =) discs head orelse
       is_some maybe_rhs andalso
         member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then
-      dissect_coeqn_disc seq fun_names basic_ctr_specss NONE NONE prems concl matchedsss
+      dissect_coeqn_disc sequential fun_names basic_ctr_specss NONE NONE prems concl matchedsss
       |>> single
     else if member (op =) sels head then
-      ([dissect_coeqn_sel fun_names basic_ctr_specss NONE NONE eqn' maybe_of_spec concl], matchedsss)
+      ([dissect_coeqn_sel fun_names basic_ctr_specss NONE NONE eqn' maybe_of_spec concl],
+       matchedsss)
     else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
       member (op =) ctrs (head_of (unfold_let (the maybe_rhs))) then
-      dissect_coeqn_ctr seq fun_names basic_ctr_specss eqn' NONE prems concl matchedsss
+      dissect_coeqn_ctr sequential fun_names basic_ctr_specss eqn' NONE prems concl matchedsss
     else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
       null prems then
       dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn' concl matchedsss
@@ -852,14 +853,14 @@
         [] => ()
       | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
 
-    val seq = member (op =) opts Sequential_Option;
+    val sequential = member (op =) opts Sequential_Option;
     val exhaustive = member (op =) opts Exhaustive_Option;
 
     val fun_names = map Binding.name_of bs;
     val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
     val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
     val eqns_data =
-      fold_map2 (dissect_coeqn lthy seq has_call fun_names basic_ctr_specss) (map snd specs)
+      fold_map2 (dissect_coeqn lthy sequential has_call fun_names basic_ctr_specss) (map snd specs)
         maybe_of_specs []
       |> flat o fst;
 
@@ -903,8 +904,10 @@
       build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
 
     fun exclude_tac (c, c', a) =
-      if a orelse c = c' orelse seq then SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
-      else maybe_tac;
+      if a orelse c = c' orelse sequential then
+        SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
+      else
+        maybe_tac;
 
 (*
 val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^