--- a/Nominal/nominal_mutual.ML	Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_mutual.ML	Sat Jan 11 23:17:23 2014 +0000
@@ -171,7 +171,7 @@
     val rhs = inst pre_rhs
 
     val cqs = map (cterm_of thy) qs
-    val ags = map (Thm.assume o cterm_of thy) gs
+    val (ags, ctxt') = fold_map Thm.assume_hyps (map (cterm_of thy) gs) ctxt
 
     val import = fold Thm.forall_elim cqs
       #> fold Thm.elim_implies ags
@@ -179,7 +179,7 @@
     val export = fold_rev (Thm.implies_intr o cprop_of) ags
       #> fold_rev forall_intr_rename (oqnames ~~ cqs)
   in
-    F ctxt (f, qs, gs, args, rhs) import export
+    F ctxt' (f, qs, gs, args, rhs) import export
   end
 
 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
@@ -188,17 +188,19 @@
     val (MutualPart {f=SOME f, ...}) = get_part fname parts
  
     val psimp = import sum_psimp_eq
-    val (simp, restore_cond) =
+    val ((simp, restore_cond), ctxt') =
       case cprems_of psimp of
-        [] => (psimp, I)
-      | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
+        [] => ((psimp, I), ctxt)
+      | [cond] =>
+          let val (asm, ctxt') = Thm.assume_hyps cond ctxt
+          in ((Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end
       | _ => raise General.Fail "Too many conditions"
   in
-    Goal.prove ctxt [] []
+    Goal.prove ctxt' [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
-         THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac ctxt) 1)
+      (fn _ => (Local_Defs.unfold_tac ctxt' all_orig_fdefs)
+         THEN EqSubst.eqsubst_tac ctxt' [0] [simp] 1
+         THEN (simp_tac ctxt') 1)
     |> restore_cond
     |> export
   end
@@ -212,19 +214,21 @@
     val (MutualPart {f=SOME f, ...}) = get_part fname parts
     
     val psimp = import sum_psimp_eq
-    val (cond, simp, restore_cond) =
+    val ((cond, simp, restore_cond), ctxt') =
       case cprems_of psimp of
-        [] => ([], psimp, I)
-      | [cond] => ([Thm.assume cond], Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
+        [] => (([], psimp, I), ctxt)
+      | [cond] =>
+          let val (asm, ctxt') = Thm.assume_hyps cond ctxt
+          in (([asm], Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end
       | _ => raise General.Fail "Too many conditions"
 
-    val ([p], ctxt') = ctxt
+    val ([p], ctxt'') = ctxt'
       |> fold Variable.declare_term args  
       |> Variable.variant_fixes ["p"] 		   
     val p = Free (p, @{typ perm})
 
     val simpset =
-      put_simpset HOL_basic_ss ctxt' addsimps 
+      put_simpset HOL_basic_ss ctxt'' addsimps 
       @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @
       @{thms Projr.simps Projl.simps} @
       [(cond MRS eqvt_thm) RS @{thm sym}] @ 
@@ -232,10 +236,10 @@
     val goal_lhs = mk_perm p (list_comb (f, args))
     val goal_rhs = list_comb (f, map (mk_perm p) args)
   in
-    Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs))
-      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+    Goal.prove ctxt'' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs))
+      (fn _ => Local_Defs.unfold_tac ctxt'' all_orig_fdefs
          THEN (asm_full_simp_tac simpset 1))
-    |> singleton (Proof_Context.export ctxt' ctxt)
+    |> singleton (Proof_Context.export ctxt'' ctxt)
     |> restore_cond
     |> export
   end