--- a/Nominal/nominal_dt_rawfuns.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -125,7 +125,7 @@
       val raw_bn_eqs = the simps
 
       val raw_bn_info = 
-        prep_bn_info lthy raw_dt_names raw_dts fs (map prop_of raw_bn_eqs)
+        prep_bn_info lthy raw_dt_names raw_dts fs (map Thm.prop_of raw_bn_eqs)
     in
       (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
     end
@@ -166,7 +166,7 @@
       binders
       |> map (bind_fn lthy args)
       |> split_list
-      |> pairself combine_fn
+      |> apply2 combine_fn
     end  
 
     val t1 = map (mk_fv_body fv_map args) bodies
@@ -199,7 +199,7 @@
 
 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = 
   let
-    val arg_names = Datatype_Prop.make_tnames arg_tys
+    val arg_names = Old_Datatype_Prop.make_tnames arg_tys
     val args = map Free (arg_names ~~ arg_tys)
     val fv = lookup fv_map ty
     val lhs = fv $ list_comb (constr, args)
@@ -211,7 +211,7 @@
 
 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
   let
-    val arg_names = Datatype_Prop.make_tnames arg_tys
+    val arg_names = Old_Datatype_Prop.make_tnames arg_tys
     val args = map Free (arg_names ~~ arg_tys)
     val fv_bn = lookup fv_bn_map bn_trm
     val lhs = fv_bn $ list_comb (constr, args)
@@ -287,7 +287,7 @@
 fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) =
   let
     val p = Free ("p", @{typ perm})
-    val arg_names = Datatype_Prop.make_tnames arg_tys
+    val arg_names = Old_Datatype_Prop.make_tnames arg_tys
     val args = map Free (arg_names ~~ arg_tys)
     val perm_bn = lookup perm_bn_map bn_trm
     val lhs = perm_bn $ p $ list_comb (constr, args)
@@ -347,7 +347,7 @@
 fun prove_permute_zero induct perm_defs perm_fns ctxt =
   let
     val perm_types = map (body_type o fastype_of) perm_fns
-    val perm_indnames = Datatype_Prop.make_tnames perm_types
+    val perm_indnames = Old_Datatype_Prop.make_tnames perm_types
   
     fun single_goal ((perm_fn, T), x) =
       HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
@@ -358,11 +358,11 @@
 
     val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs)
 
-    val tac = (Datatype_Aux.ind_tac induct perm_indnames 
+    val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames 
                THEN_ALL_NEW asm_simp_tac simpset) 1
   in
     Goal.prove ctxt perm_indnames [] goals (K tac)
-    |> Datatype_Aux.split_conj_thm
+    |> Old_Datatype_Aux.split_conj_thm
   end
 
 
@@ -371,7 +371,7 @@
     val p = Free ("p", @{typ perm})
     val q = Free ("q", @{typ perm})
     val perm_types = map (body_type o fastype_of) perm_fns
-    val perm_indnames = Datatype_Prop.make_tnames perm_types
+    val perm_indnames = Old_Datatype_Prop.make_tnames perm_types
   
     fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 
       (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
@@ -383,11 +383,11 @@
     (* FIXME proper goal context *)
     val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs)
 
-    val tac = (Datatype_Aux.ind_tac induct perm_indnames
+    val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
                THEN_ALL_NEW asm_simp_tac simpset) 1
   in
     Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac)
-    |> Datatype_Aux.split_conj_thm 
+    |> Old_Datatype_Aux.split_conj_thm 
   end
 
 
@@ -403,7 +403,7 @@
       fastype_of cnstr
       |> strip_type
 
-    val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+    val arg_names = Name.variant_list ["p"] (Old_Datatype_Prop.make_tnames arg_tys)
     val args = map Free (arg_names ~~ arg_tys)
 
     val lhs = lookup_perm p (ty, list_comb (cnstr, args))
@@ -430,8 +430,8 @@
 
     val perm_eqs = map (mk_perm_eq (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns)
 
-    fun tac _ (_, _, simps) =
-      Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+    fun tac ctxt (_, _, simps) =
+      Class.intro_classes_tac ctxt [] THEN ALLGOALS (resolve_tac ctxt simps)
   
     fun morphism phi (fvs, dfs, simps) =
       (map (Morphism.term phi) fvs, 
@@ -442,7 +442,7 @@
       lthy
       |> Local_Theory.exit_global
       |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt}) 
-      |> Primrec.add_primrec perm_fn_binds perm_eqs
+      |> BNF_LFP_Compat.primrec perm_fn_binds perm_eqs
     
     val perm_zero_thms = prove_permute_zero raw_induct_thm perm_eq_thms perm_funs lthy'
     val perm_plus_thms = prove_permute_plus raw_induct_thm perm_eq_thms perm_funs lthy'  
@@ -468,7 +468,7 @@
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
   HEADGOAL
     (Object_Logic.full_atomize_tac ctxt
-     THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))  
+     THEN' (DETERM o (Induct_Tacs.induct_tac ctxt insts (SOME ind_thms)))
      THEN_ALL_NEW  subproof_tac const_names simps ctxt)
 
 fun mk_eqvt_goal pi const arg =
@@ -491,13 +491,13 @@
         |> map fastype_of
         |> map domain_type 
       val (arg_names, ctxt'') = 
-        Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
+        Variable.variant_fixes (Old_Datatype_Prop.make_tnames arg_tys) ctxt'
       val args = map Free (arg_names ~~ arg_tys)
       val goals = map2 (mk_eqvt_goal p) consts args
       val insts = map (single o SOME) arg_names
       val const_names = map (fst o dest_Const) consts      
     in
-      Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
+      Goal.prove_common ctxt'' NONE [] [] goals (fn {context, ...} => 
         prove_eqvt_tac insts ind_thms const_names simps context)
       |> Proof_Context.export ctxt'' ctxt
     end