tuning
authorblanchet
Mon Oct 21 09:31:19 2013 +0200 (2013-10-21)
changeset 541801753c57eb16c
parent 54179 c1daa6e05565
child 54181 66edcd52daeb
tuning
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Oct 21 09:14:05 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Oct 21 09:31:19 2013 +0200
     1.3 @@ -37,8 +37,8 @@
     1.4  (* TODO: test with sort constraints on As *)
     1.5  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
     1.6     as deads? *)
     1.7 -fun mutualize_fp_sugars mutualize fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
     1.8 -  if mutualize orelse has_duplicates (op =) fpTs then
     1.9 +fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
    1.10 +  if has_nested orelse has_duplicates (op =) fpTs then
    1.11      let
    1.12        val thy = Proof_Context.theory_of no_defs_lthy0;
    1.13  
    1.14 @@ -251,13 +251,13 @@
    1.15      val perm_kks = permute kks;
    1.16      val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
    1.17  
    1.18 -    val mutualize = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts;
    1.19 +    val has_nested = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts;
    1.20      val perm_callssss = pad_and_indexify_calls perm_fp_sugars0 nn actual_callssss0;
    1.21  
    1.22      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
    1.23  
    1.24      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
    1.25 -      mutualize_fp_sugars mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.26 +      mutualize_fp_sugars has_nested fp perm_bs perm_Ts get_perm_indices perm_callssss
    1.27          perm_fp_sugars0 lthy;
    1.28  
    1.29      val fp_sugars = unpermute perm_fp_sugars;
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 09:14:05 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 09:31:19 2013 +0200
     2.3 @@ -896,7 +896,7 @@
     2.4      val exclss'' = exclss' |> map (map (fn (idx, t) =>
     2.5        (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (excl_tac idx), t))));
     2.6      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
     2.7 -    val (obligation_idxss, goalss) = exclss''
     2.8 +    val (goal_idxss, goalss) = exclss''
     2.9        |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
    2.10        |> split_list o map split_list;
    2.11  
    2.12 @@ -904,7 +904,7 @@
    2.13        let
    2.14          val def_thms = map (snd o snd) def_thms';
    2.15  
    2.16 -        val exclss' = map (op ~~) (obligation_idxss ~~ thmss');
    2.17 +        val exclss' = map (op ~~) (goal_idxss ~~ thmss');
    2.18          fun mk_exclsss excls n =
    2.19            (excls, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
    2.20            |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])));