# HG changeset patch
# User blanchet
# Date 1410775901 -7200
# Node ID 5f6f48e87de69e5983b773b29190e17975da4728
# Parent  f6af48bd7c04e65ab596d7adff9dc3bdf7b9dbb5
tuning

diff -r f6af48bd7c04 -r 5f6f48e87de6 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 15 11:54:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 15 12:11:41 2014 +0200
@@ -47,8 +47,8 @@
     Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
   end;
 
-fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
-    (absT_infos : absT_info list) lthy =
+fun construct_mutualized_fp fp mutual_cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss)
+    bnfs (absT_infos : absT_info list) lthy =
   let
     fun of_fp_res get =
       map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
@@ -273,15 +273,15 @@
           map (typ_subst_nonatomic_sorted (map (rpair dummyT)
             (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
 
-        val (clique, TUs) =
+        val (mutual_clique, TUs) =
           map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
           |>> map subst
           |> `(fn (_, Ys) =>
-            nth cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
+            nth mutual_cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
           ||> uncurry (map2 mk_co_algT);
-        val cands = cliques ~~ map2 mk_co_algT fold_preTs' Xs;
+        val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs;
         val js = find_indices (fn ((cl, cand), TU) =>
-          cl = clique andalso Type.could_unify (TU, cand)) TUs cands;
+          cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands;
         val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
       in
         force_typ names_lthy (Tpats ---> TU) raw_rec
diff -r f6af48bd7c04 -r 5f6f48e87de6 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 15 11:54:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 15 12:11:41 2014 +0200
@@ -117,7 +117,7 @@
   |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
   |> map_filter I;
 
-fun mutualize_fp_sugars plugins fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
+fun mutualize_fp_sugars plugins fp mutual_cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
   let
     val thy = Proof_Context.theory_of no_defs_lthy;
 
@@ -240,8 +240,8 @@
 
         val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
                dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
-          fp_bnf (construct_mutualized_fp fp cliques unsorted_fpTs fp_sugars0) fp_bs unsorted_As'
-            killed_As' fp_eqs no_defs_lthy;
+          fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs
+            unsorted_As' killed_As' fp_eqs no_defs_lthy;
 
         val fp_abs_inverses = map #abs_inverse fp_absT_infos;
         val fp_type_definitions = map #type_definition fp_absT_infos;
@@ -421,7 +421,7 @@
       | gather_types _ _ _ _ (T :: _) = not_co_datatype T;
 
     val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts;
-    val (perm_cliques, perm_Ts) =
+    val (perm_mutual_cliques, perm_Ts) =
       split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss));
 
     val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
@@ -441,10 +441,10 @@
     fun permute xs = permute_like (op =) Ts perm_Ts xs;
     fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
 
-    (* The assignment of callers to cliques is incorrect in general. This code would need to inspect
-       the actual calls to discover the correct cliques in the presence of type duplicates. However,
-       the naive scheme implemented here supports "prim(co)rec" specifications following reasonable
-       ordering of the duplicates (e.g., keeping the cliques together). *)
+    (* The assignment of callers to mutual cliques is incorrect in general. This code would need to
+       inspect the actual calls to discover the correct cliques in the presence of type duplicates.
+       However, the naive scheme implemented here supports "prim(co)rec" specifications following
+       reasonable ordering of the duplicates (e.g., keeping the cliques together). *)
     val perm_bs = permute bs;
     val perm_callers = permute callers;
     val perm_kks = permute kks;
@@ -457,7 +457,7 @@
       if length perm_Tss = 1 then
         ((perm_fp_sugars0, (NONE, NONE)), lthy)
       else
-        mutualize_fp_sugars plugins fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers
+        mutualize_fp_sugars plugins fp perm_mutual_cliques perm_bs perm_frozen_gen_Ts perm_callers
           perm_callssss perm_fp_sugars0 lthy;
 
     val fp_sugars = unpermute perm_fp_sugars;
diff -r f6af48bd7c04 -r 5f6f48e87de6 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 15 11:54:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 15 12:11:41 2014 +0200
@@ -262,7 +262,7 @@
 
     (* put nested types before the types that nest them, as needed for N2M *)
     val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs);
-    val (cliques, descr) =
+    val (mutual_cliques, descr) =
       split_list (flat (map_index (fn (i, descr) => map (pair i) descr)
         (maps cliquify_descr descrs)));
 
@@ -286,8 +286,8 @@
 
     val ((fp_sugars', (lfp_sugar_thms', _)), lthy') =
       if nn > nn_fp then
-        mutualize_fp_sugars (K true) Least_FP cliques compat_bs fpTs' callers callssss fp_sugars
-          lthy
+        mutualize_fp_sugars (K true) Least_FP mutual_cliques compat_bs fpTs' callers callssss
+          fp_sugars lthy
       else
         ((fp_sugars, (NONE, NONE)), lthy);