diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_library.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -86,7 +86,7 @@
   (* datatype operations *)
   type cns_info = (term * typ * typ list * bool list) list
 
-  val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list
+  val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list
 
   (* tactics for function package *)
   val size_ss: simpset
@@ -333,10 +333,10 @@
   let
     fun aux ((ty_name, vs), (cname, args)) =
       let
-        val vs_tys = map (Datatype_Aux.typ_of_dtyp descr) vs
+        val vs_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) vs
         val ty = Type (ty_name, vs_tys)
-        val arg_tys = map (Datatype_Aux.typ_of_dtyp descr) args
-        val is_rec = map Datatype_Aux.is_rec_type args
+        val arg_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) args
+        val is_rec = map Old_Datatype_Aux.is_rec_type args
       in
         (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
       end
@@ -451,13 +451,13 @@
     val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def}
   in
     EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
-      REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac monos)),
-      REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
+      REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)),
+      REPEAT_DETERM (rtac impI 1 THEN (assume_tac ctxt 1 ORELSE tac))]
   end
 
 fun map_thm ctxt f tac thm =
   let
-    val opt_goal_trm = map_term f (prop_of thm)
+    val opt_goal_trm = map_term f (Thm.prop_of thm)
   in
     case opt_goal_trm of
       NONE => thm
@@ -495,7 +495,7 @@
 fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars;
 fun atomize_rule ctxt i thm =
   Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm
-fun atomize_concl ctxt thm = atomize_rule ctxt (length (prems_of thm)) thm
+fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm
 
 
 (* applies a tactic to a formula composed of conjunctions *)