diff -r a44479bde681 -r 017e33849f4d Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Nominal2.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -46,7 +46,7 @@
 val induct_attr = Attrib.internal (K Induct.induct_simp_add)
 *}
 
-section{* Interface for nominal_datatype *}
+section{* Interface for @{text nominal_datatype} *}
 
 ML {*
 fun get_cnstrs dts =
@@ -64,7 +64,7 @@
 *}
 
 
-text {* Infrastructure for adding "_raw" to types and terms *}
+text {* Infrastructure for adding @{text "_raw"} to types and terms *}
 
 ML {*
 fun add_raw s = s ^ "_raw"
@@ -109,7 +109,7 @@
     (raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs
   
   val bn_eqs' = map (fn (attr, trm) => 
-    (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
+    ((attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm), [], [])) bn_eqs
 in
   (bn_funs', bn_eqs') 
 end 
@@ -260,15 +260,15 @@
 
   val raw_fv_eqvt = 
     raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) 
-      (Local_Theory.restore lthy_tmp)
+      (Local_Theory.reset lthy_tmp)
     
   val raw_size_eqvt =
     let
       val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info
     in
       raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) 
-        (Local_Theory.restore lthy_tmp)
-        |> map (rewrite_rule (Local_Theory.restore lthy_tmp)
+        (Local_Theory.reset lthy_tmp)
+        |> map (rewrite_rule (Local_Theory.reset lthy_tmp)
             @{thms permute_nat_def[THEN eq_reflection]})
         |> map (fn thm => thm RS @{thm sym})
     end 
@@ -489,7 +489,7 @@
   (* generating the prefix for the theorem names *)
   val thms_name = 
     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
-  fun thms_suffix s = Binding.qualified true s thms_name 
+  fun thms_suffix s = Binding.qualify_name true thms_name s
   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
   val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms
@@ -582,7 +582,7 @@
   val lthy = Named_Target.theory_init thy
 
   val ((bn_funs, bn_eqs), lthy') = 
-    Specification.read_spec bn_fun_strs bn_eq_strs lthy
+    Specification.read_multi_specs bn_fun_strs bn_eq_strs lthy
 
   fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
   
@@ -727,7 +727,7 @@
 
 (* binding function parser *)
 val bnfun_parser = 
-  Scan.optional (@{keyword "binder"} |-- Parse.fixes -- Parse_Spec.where_alt_specs) ([], [])
+  Scan.optional (@{keyword "binder"} |-- Parse_Spec.specification) ([], [])
 
 (* main parser *)
 val main_parser =