src/HOL/Nominal/nominal_induct.ML

       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS
             let
               val adefs = nth_list atomized_defs (j - 1);
-              val frees = fold (Term.add_frees o prop_of) adefs [];
+              val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
               val xs = nth_list fixings (j - 1);
               val k = nth concls (j - 1) + more_consumes
             in
               Method.insert_tac (more_facts @ adefs) THEN'
                 (if simp then