src/HOL/Nominal/nominal_inductive.ML

       (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
     fun eqvt_tac pi (intr, vs) st =
       let
         fun eqvt_err s = error
           ("Could not prove equivariance for introduction rule\n" ^
-           Sign.string_of_term (theory_of_thm intr)
+           Syntax.string_of_term_global (theory_of_thm intr)
              (Logic.unvarify (prop_of intr)) ^ "\n" ^ s);
         val res = SUBPROOF (fn {prems, params, ...} =>
           let
             val prems' = map (fn th => the_default th (map_thm ctxt
               (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;

           in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
           end) ctxt 1 st
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
           NONE => eqvt_err ("Rule does not match goal\n" ^
-            Sign.string_of_term (theory_of_thm st) (hd (prems_of st)))
+            Syntax.string_of_term_global (theory_of_thm st) (hd (prems_of st)))
         | SOME (th, _) => Seq.single th
       end;
     val thss = map (fn atom =>
       let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
       in map (fn th => zero_var_indexes (th RS mp))