src/HOL/Tools/BNF/bnf_fp_util.ML
changeset 62621 a1e73be79c0b
parent 62335 e85c42f4f30a
child 62684 cb20e8828196
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 14 15:58:02 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 14 21:37:49 2016 +0100
@@ -626,7 +626,7 @@
     val ((bnfs, (deadss, livess)), accum) =
       apfst (apsnd split_list o split_list)
         (@{fold_map 2}
-          (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
+          (fn b => bnf_of_typ true Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
           ((empty_comp_cache, empty_unfolds), lthy));
 
     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))