--- a/Nominal/nominal_dt_rawfuns.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -11,7 +11,7 @@
   val is_recursive_binder: bclause -> bool
 
   val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> 
-    (Attrib.binding * term) list -> local_theory ->
+    Specification.multi_specs -> local_theory ->
     (term list * thm list * bn_info list * thm list * local_theory) 
 
   val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> 
@@ -118,7 +118,7 @@
       val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
         Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy
 
-      val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.restore lthy1)
+      val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.reset lthy1)  (* FIXME disrupts context *)
       val {fs, simps, inducts, ...} = info
 
       val raw_bn_induct = (the inducts)
@@ -252,12 +252,12 @@
     val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_cns_info bclausesss) bn_info
   
     val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
-    val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
+    val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat fv_eqs @ flat fv_bn_eqs)
 
     val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
       Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy
 
-    val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
+    val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.reset lthy')  (* FIXME disrupts context *)
  
     val {fs, simps, inducts, ...} = info; 
 
@@ -324,7 +324,7 @@
       val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info
 
       val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names
-      val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs)
+      val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat perm_bn_eqs)
 
       val prod_simps = @{thms prod.inject HOL.simp_thms}
 
@@ -332,7 +332,7 @@
         Function_Common.default_config 
           (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) lthy
     
-      val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy')
+      val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.reset lthy')  (* FIXME disrupts context *)
 
       val {fs, simps, ...} = info;
 
@@ -412,7 +412,7 @@
   
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))  
   in
-    (Attrib.empty_binding, eq)
+    ((Binding.empty_atts, eq), [], [])
   end