# HG changeset patch
# User wenzelm
# Date 1447433313 -3600
# Node ID ffee6aea0ff2256b2f4c2d5a332c92866bbc71da
# Parent  5dce70aecbfca12d8d3b4b638306bb625984789c
preserve names of for-fixes for faithfully;

diff -r 5dce70aecbfc -r ffee6aea0ff2 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 13 16:02:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 13 17:48:33 2015 +0100
@@ -9470,7 +9470,7 @@
   have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
     unfolding split_def setsum_subtractf ..
   also have "\<dots> \<le> e + k"
-    apply (rule *[OF **, where ir2="setsum (\<lambda>k. integral k f) r"])
+    apply (rule *[OF **, where ir1="setsum (\<lambda>k. integral k f) r"])
   proof goal_cases
     case 1
     have *: "k * real (card r) / (1 + real (card r)) < k"
diff -r 5dce70aecbfc -r ffee6aea0ff2 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Nov 13 16:02:59 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Nov 13 17:48:33 2015 +0100
@@ -1066,12 +1066,13 @@
       Assumption.add_assms
         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
 
-    val (assumes_bindings, shows_bindings) =
-      apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
-
+    (*params*)
     val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
       |> prep_clause prep_var prep_propp raw_fixes (map snd raw_assumes) (map snd raw_shows);
 
+    (*prems*)
+    val (assumes_bindings, shows_bindings) =
+      apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
     val (that_fact, goal_ctxt) = params_ctxt
       |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
       |> (fn (premss, ctxt') =>
@@ -1086,10 +1087,21 @@
                   (assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
           in (prems, ctxt'') end);
 
-    fun after_qed' (result_ctxt, results) state' = state'
-      |> local_results (shows_bindings ~~ burrow (Proof_Context.export result_ctxt ctxt) results)
-      |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
-      |> after_qed (result_ctxt, results);
+    (*result*)
+    fun after_qed' (result_ctxt, results) state' =
+      let
+        val ctxt' = context_of state';
+        val export0 =
+          Assumption.export false result_ctxt ctxt' #>
+          fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #>
+          Raw_Simplifier.norm_hhf_protect ctxt';
+        val export = map export0 #> Variable.export result_ctxt ctxt';
+      in
+        state'
+        |> local_results (shows_bindings ~~ burrow export results)
+        |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
+        |> after_qed (result_ctxt, results)
+      end;
   in
     state
     |> generic_goal kind before_qed (after_qed', K I) goal_ctxt shows_propss result_binds