diff -r b2e1a7b83e05 -r 67370521c09c Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Nominal2.thy	Thu Jul 09 02:32:46 2015 +0100
@@ -149,7 +149,7 @@
   val bn_fun_strs = get_bn_fun_strs bn_funs
   val bn_fun_strs' = add_raws bn_fun_strs
   val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
-  val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) 
+  val bn_fun_full_env = map (apply2 (Long_Name.qualify thy_name)) 
     (bn_fun_strs ~~ bn_fun_strs')
   
   val raw_dts = rawify_dts dts dts_env
@@ -157,14 +157,14 @@
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses 
 
   val (raw_full_dt_names', thy1) = 
-    Datatype.add_datatype Datatype.default_config raw_dts thy
+    Old_Datatype.add_datatype Old_Datatype_Aux.default_config raw_dts thy
 
   val lthy1 = Named_Target.theory_init thy1
 
-  val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' 
+  val dtinfos = map (Old_Datatype_Data.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' 
   val {descr, ...} = hd dtinfos
 
-  val raw_tys = Datatype_Aux.get_rec_types descr
+  val raw_tys = Old_Datatype_Aux.get_rec_types descr
   val raw_ty_args = hd raw_tys
     |> snd o dest_Type
     |> map dest_TFree 
@@ -179,7 +179,7 @@
   val raw_exhaust_thms = map #exhaust dtinfos
   val raw_size_trms = map HOLogic.size_const raw_tys
   val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd)
-    (BNF_LFP_Size.lookup_size lthy1 (hd raw_full_dt_names')))
+    (BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names')))
 
   val raw_result = RawDtInfo 
     {raw_dt_names = raw_full_dt_names',
@@ -303,7 +303,7 @@
   val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux
 
   fun match_const cnst th =
-    (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th =
+    (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o Thm.prop_of) th =
     fst (dest_Const cnst);
   fun find_matching_rsp cnst =
     hd (filter (fn th => match_const cnst th) raw_funs_rsp);
@@ -398,7 +398,7 @@
   val qperm_bns = map #qconst qperm_bns_info
 
   val _ = trace_msg (K "Lifting of theorems...")  
-  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def
+  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_sel
     prod.case} 
 
   val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, 
@@ -452,7 +452,7 @@
 
   val qsupp_constrs = qfv_defs
     |> map (simplify (put_simpset HOL_basic_ss lthyC
-        addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms)))
+        addsimps (filter (is_qfv_thm o Thm.prop_of) qfv_supp_thms)))
 
   val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
   val transform_thms = 
@@ -548,7 +548,7 @@
     ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx')))
 
   val (dts, spec_ctxt) = 
-    Datatype.read_specs (map prep_spec dt_strs) thy
+    Old_Datatype.read_specs (map prep_spec dt_strs) thy
  
   fun augment ((tname, tvs, mx), constrs) =
     ((tname, map (apsnd (augment_sort thy)) tvs, mx), 
@@ -736,10 +736,9 @@
 end
 
 (* Command Keyword *)
-val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"}
+val _ = Outer_Syntax.local_theory @{command_keyword nominal_datatype}
   "declaration of nominal datatypes" 
     (main_parser >> nominal_datatype2_cmd)
 *}
 
-
 end