src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

               in
                 (case rhs_info_opt of
                   NONE => []
                 | SOME (exhaustive_code, rhs, raw_rhs, ctr_thms) =>
                   let
-                    val ms = map (Logic.count_prems o prop_of) ctr_thms;
+                    val ms = map (Logic.count_prems o Thm.prop_of) ctr_thms;
                     val (raw_goal, goal) = (raw_rhs, rhs)
                       |> apply2 (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
                         #> curry Logic.list_all (map dest_Free fun_args));
                     val (distincts, discIs, _, split_sels, split_sel_asms) =
                       case_thms_of_term lthy raw_rhs;