diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_atoms.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -12,7 +12,7 @@
   val add_atom_decl: (binding * (binding option)) -> theory -> theory
 end;
 
-structure Atom_Decl :> ATOM_DECL =
+structure Atom_Decl : ATOM_DECL =
 struct
 
 val simp_attr = Attrib.internal (K Simplifier.simp_add)
@@ -32,9 +32,9 @@
 
     (* typedef *)
     val set = atom_decl_set str;
-    fun tac _ = rtac @{thm exists_eq_simple_sort} 1;
+    fun tac ctxt = resolve_tac ctxt @{thms exists_eq_simple_sort} 1;
     val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
-      Typedef.add_typedef_global false (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef_global {overloaded = false} (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type (fst info);
@@ -68,7 +68,7 @@
     val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def]
     val thy = lthy
       |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm]))
-      |> Class.prove_instantiation_instance (K (rtac class_thm 1))
+      |> Class.prove_instantiation_instance (fn ctxt => resolve_tac ctxt [class_thm] 1)
       |> Local_Theory.exit_global;
   in
     thy