changeset 58179 | 2de7b0313de3 |
parent 58131 | 1abeda3c3bc2 |
child 58180 | 95397823f39e |
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 04 09:02:43 2014 +0200 @@ -113,8 +113,7 @@ |> map_filter I; (* TODO: test with sort constraints on As *) -fun mutualize_fp_sugars fp cliques bs fpTs callers callssss (fp_sugars0 as fp_sugars01 :: _) - no_defs_lthy0 = +fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy0 = let val thy = Proof_Context.theory_of no_defs_lthy0;