# HG changeset patch
# User blanchet
# Date 1383770441 -3600
# Node ID 32b5c4821d9dd467e3ceec69c57f7c9bed46e4e1
# Parent  b01057e722336083373264a4d38f4bf1ced47a49
tuning

diff -r b01057e72233 -r 32b5c4821d9d src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 21:23:42 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 21:40:41 2013 +0100
@@ -292,20 +292,20 @@
     val perm_actual_Ts as Type (_, tyargs0) :: _ =
       sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
 
+    fun the_fp_sugar_of (T as Type (T_name, _)) =
+      (case fp_sugar_of lthy T_name of
+        SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T
+      | NONE => not_co_datatype T);
+
     fun check_enrich_with_mutuals _ [] = []
-      | check_enrich_with_mutuals seen ((T as Type (T_name, tyargs)) :: Ts) =
-        (case fp_sugar_of lthy T_name of
-          SOME ({fp = fp', fp_res = {Ts = Ts', ...}, ...}) =>
-          if fp = fp' then
-            let
-              val mutual_Ts = map (fn Type (s, _) => Type (s, tyargs)) Ts';
-              val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
-            in
-              mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'
-            end
-          else
-            not_co_datatype T
-        | NONE => not_co_datatype T)
+      | check_enrich_with_mutuals seen ((T as Type (_, tyargs)) :: Ts) =
+        let
+          val {fp_res = {Ts = Ts', ...}, ...} = the_fp_sugar_of T
+          val mutual_Ts = map (fn Type (s, _) => Type (s, tyargs)) Ts';
+          val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
+        in
+          mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'
+        end
       | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T;
 
     val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts;