tuned;

--- a/src/HOL/Library/reflection.ML	Tue Nov 08 08:56:24 2011 +0100
+++ b/src/HOL/Library/reflection.ML	Tue Nov 08 11:44:37 2011 +0100
@@ -60,10 +60,11 @@
    fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
      | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
    fun tryext x = (x RS ext2 handle THM _ =>  x)
-   val cong = (Goal.prove ctxt'' [] (map mk_def env)
-                          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
-                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
-                                                        THEN rtac th' 1)) RS sym
+   val cong =
+    (Goal.prove ctxt'' [] (map mk_def env)
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
+      (fn {context, prems, ...} =>
+        Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym
 
    val (cong' :: vars') =
        Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)

--- a/src/HOL/Tools/Function/mutual.ML	Tue Nov 08 08:56:24 2011 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Tue Nov 08 11:44:37 2011 +0100
@@ -176,7 +176,7 @@
   end
 
 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
-  import (export : thm -> thm) sum_psimp_eq =
+    import (export : thm -> thm) sum_psimp_eq =
   let
     val (MutualPart {f=SOME f, ...}) = get_part fname parts
 
@@ -190,9 +190,10 @@
   in
     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 (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
+      (fn _ =>
+        Local_Defs.unfold_tac ctxt all_orig_fdefs
+          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
+          THEN (simp_tac (simpset_of ctxt)) 1)
     |> restore_cond
     |> export
   end

--- a/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 08:56:24 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 11:44:37 2011 +0100
@@ -64,7 +64,7 @@
 
 (*rewrite conclusion with k-th assumtion*)
 fun rewrite_with_asm_tac ctxt k =
-  Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
+  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
     Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
 
 fun dest_case thy t =