src/HOL/Nominal/nominal_inductive.ML

 fun first_order_matchs pats objs = Thm.first_order_match
   (eta_contract_cterm (Conjunction.mk_conjunction_balanced pats),
    eta_contract_cterm (Conjunction.mk_conjunction_balanced objs));
 
 fun first_order_mrs ths th = ths MRS
-  Thm.instantiate (first_order_matchs (cprems_of th) (map Thm.cprop_of ths)) th;
+  Thm.instantiate (first_order_matchs (Thm.cprems_of th) (map Thm.cprop_of ths)) th;
 
 fun prove_strong_ind s avoids lthy =
   let
     val thy = Proof_Context.theory_of lthy;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =

                            else (case AList.lookup op = tab x of
                              SOME y => y
                            | NONE => fold_rev (NominalDatatype.mk_perm []) pis x)
                        | x => x) o HOLogic.dest_Trueprop o Thm.prop_of) case_hyps));
                   val inst = Thm.first_order_match (Thm.dest_arg
-                    (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj);
+                    (Drule.strip_imp_concl (hd (Thm.cprems_of case_hyp))), obj);
                   val th = Goal.prove ctxt3 [] [] (Thm.term_of concl)
                     (fn {context = ctxt4, ...} =>
                        resolve_tac ctxt4 [Thm.instantiate inst case_hyp] 1 THEN
                        SUBPROOF (fn {context = ctxt5, prems = fresh_hyps, ...} =>
                          let