src/HOL/Nominal/nominal_permeq.ML

     let val goal = List.nth(cprems_of st, i-1)
     in
       case Logic.strip_assums_concl (term_of goal) of
           _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
           let
-            val cert = Thm.cterm_of (sign_of_thm st);
+            val cert = Thm.cterm_of (Thm.theory_of_thm st);
             val ps = Logic.strip_params (term_of goal);
             val Ts = rev (map snd ps);
             val vs = collect_vars 0 x [];
             val s = Library.foldr (fn (v, s) =>
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)

         val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
     in
       case Logic.strip_assums_concl (term_of goal) of
           _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
           let
-            val cert = Thm.cterm_of (sign_of_thm st);
+            val cert = Thm.cterm_of (Thm.theory_of_thm st);
             val ps = Logic.strip_params (term_of goal);
             val Ts = rev (map snd ps);
             val vs = collect_vars 0 t [];
             val s = Library.foldr (fn (v, s) =>
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)