--- a/Nominal/nominal_dt_rawfuns.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -261,7 +261,9 @@
  
     val {fs, simps, inducts, ...} = info; 
 
-    val morphism = Proof_Context.export_morphism lthy'' lthy
+    val morphism =
+      Proof_Context.export_morphism lthy''
+        (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy)
     val simps_exp = map (Morphism.thm morphism) (the simps)
     val inducts_exp = map (Morphism.thm morphism) (the inducts)
     
@@ -334,7 +336,9 @@
 
       val {fs, simps, ...} = info;
 
-      val morphism = Proof_Context.export_morphism lthy'' lthy
+      val morphism =
+        Proof_Context.export_morphism lthy''
+          (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy)
       val simps_exp = map (Morphism.thm morphism) (the simps)
     in
       (fs, simps_exp, lthy'')
@@ -355,13 +359,12 @@
     val goals =
       HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
         (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-    val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs)
-
-    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)
+    Goal.prove ctxt perm_indnames [] goals
+      (fn {context = ctxt', ...} =>
+        (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW
+          asm_simp_tac
+            (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_zero} :: perm_defs))) 1)
     |> Old_Datatype_Aux.split_conj_thm
   end
 
@@ -379,14 +382,12 @@
     val goals =
       HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
         (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-    (* FIXME proper goal context *)
-    val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs)
-
-    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)
+    Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals
+      (fn {context = ctxt', ...} =>
+        (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW
+          asm_simp_tac
+            (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_plus} :: perm_defs))) 1)
     |> Old_Datatype_Aux.split_conj_thm 
   end