--- a/Nominal/nominal_dt_alpha.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -246,7 +246,7 @@
 
     val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
-    val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
+    val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros)
 
     val (alpha_info, lthy') = lthy
       |> Inductive.add_inductive_i
@@ -286,7 +286,7 @@
        alpha_bn_tys = alpha_bn_tys, 
        alpha_intros = alpha_intros,
        alpha_cases = alpha_cases,
-       alpha_raw_induct = alpha_raw_induct}, Local_Theory.restore lthy')
+       alpha_raw_induct = alpha_raw_induct}, Local_Theory.reset lthy')  (* FIXME disrupts context *)
   end