diff -r 332cb37cfcee -r 05392bdd2286 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Dec 29 19:37:24 2011 +0100
+++ b/src/HOL/Tools/record.ML	Thu Dec 29 20:05:53 2011 +0100
@@ -893,9 +893,9 @@
     val _ = null fields andalso raise Match;
     val u = foldr1 fields_tr' (map field_tr' fields);
   in
-    case more of
+    (case more of
       Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
-    | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
+    | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more)
   end;
 
 in
@@ -949,7 +949,7 @@
 
 (** record simprocs **)
 
-fun future_forward_prf_standard thy prf prop =
+fun future_forward_prf thy prf prop =
   let val thm =
     if ! quick_and_dirty then Skip_Proof.make_thm thy prop
     else if Goal.future_enabled () then
@@ -957,18 +957,6 @@
     else prf ()
   in Drule.export_without_context thm end;
 
-fun prove_common immediate stndrd thy asms prop tac =
-  let
-    val prv =
-      if ! quick_and_dirty then Skip_Proof.prove
-      else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
-      else Goal.prove_future;
-    val prf = prv (Proof_Context.init_global thy) [] asms prop tac;
-  in if stndrd then Drule.export_without_context prf else prf end;
-
-val prove_future_global = prove_common false;
-val prove_global = prove_common true;
-
 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   (case get_updates thy u of
     SOME u_name => u_name = s
@@ -1344,7 +1332,7 @@
     (fn thy => fn ss => fn t =>
       let
         fun prove prop =
-          prove_global true thy [] prop
+          Skip_Proof.prove_global thy [] [] prop
             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
                 addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
 
@@ -1619,11 +1607,11 @@
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
       end;
 
-    val prove_standard = prove_future_global true defs_thy;
+    val prove = Skip_Proof.prove_global defs_thy;
 
     val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
       simplify HOL_ss
-        (prove_standard [] inject_prop
+        (prove [] [] inject_prop
           (fn _ =>
             simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
             REPEAT_DETERM
@@ -1655,7 +1643,7 @@
 
 
     val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
-      prove_standard [] split_meta_prop
+      prove [] [] split_meta_prop
         (fn _ =>
           EVERY1
            [rtac equal_intr_rule, Goal.norm_hhf_tac,
@@ -1665,7 +1653,7 @@
 
     val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
       let val (assm, concl) = induct_prop in
-        prove_standard [assm] concl
+        prove [] [assm] concl
           (fn {prems, ...} =>
             cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
             resolve_tac prems 2 THEN
@@ -2139,28 +2127,19 @@
 
     (* 3rd stage: thms_thy *)
 
-    fun prove stndrd = prove_future_global stndrd defs_thy;
-    val prove_standard = prove_future_global true defs_thy;
-    val future_forward_prf = future_forward_prf_standard defs_thy;
-
-    fun prove_simp stndrd ss simps =
+    val prove = Skip_Proof.prove_global defs_thy;
+
+    fun prove_simp ss simps =
       let val tac = simp_all_tac ss simps
-      in fn prop => prove stndrd [] prop (K tac) end;
+      in fn prop => prove [] [] prop (K tac) end;
 
     val ss = get_simpset defs_thy;
 
     val sel_convs = timeit_msg ctxt "record sel_convs proof:" (fn () =>
-      map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props);
-
-    val sel_convs_standard = timeit_msg ctxt "record sel_convs_standard proof:" (fn () =>
-      map Drule.export_without_context sel_convs);
+      map (prove_simp ss (sel_defs @ accessor_thms)) sel_conv_props);
 
     val upd_convs = timeit_msg ctxt "record upd_convs proof:" (fn () =>
-      map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props);
-
-    val upd_convs_standard =
-      timeit_msg ctxt "record upd_convs_standard proof:" (fn () =>
-        map Drule.export_without_context upd_convs);
+      map (prove_simp ss (upd_defs @ updator_thms)) upd_conv_props);
 
     val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
       let
@@ -2172,7 +2151,7 @@
     val parent_induct = Option.map #induct_scheme (try List.last parents);
 
     val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () =>
-      prove_standard [] induct_scheme_prop
+      prove [] [] induct_scheme_prop
         (fn _ =>
           EVERY
            [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
@@ -2181,7 +2160,7 @@
 
     val induct = timeit_msg ctxt "record induct proof:" (fn () =>
       let val (assm, concl) = induct_prop in
-        prove_standard [assm] concl (fn {prems, ...} =>
+        prove [] [assm] concl (fn {prems, ...} =>
           try_param_tac rN induct_scheme 1
           THEN try_param_tac "more" @{thm unit.induct} 1
           THEN resolve_tac prems 1)
@@ -2198,10 +2177,10 @@
         in Object_Logic.rulify (mp OF [ind, refl]) end;
 
     val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
-      future_forward_prf cases_scheme_prf cases_scheme_prop);
+      future_forward_prf defs_thy cases_scheme_prf cases_scheme_prop);
 
     val cases = timeit_msg ctxt "record cases proof:" (fn () =>
-      prove_standard [] cases_prop
+      prove [] [] cases_prop
         (fn _ =>
           try_param_tac rN cases_scheme 1 THEN
           simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]));
@@ -2212,7 +2191,7 @@
           get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});
         val init_ss = HOL_basic_ss addsimps ext_defs;
       in
-        prove_standard [] surjective_prop
+        prove [] [] surjective_prop
           (fn _ =>
             EVERY
              [rtac surject_assist_idE 1,
@@ -2223,7 +2202,7 @@
       end);
 
     val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
-      prove false [] split_meta_prop
+      prove [] [] split_meta_prop
         (fn _ =>
           EVERY1
            [rtac equal_intr_rule, Goal.norm_hhf_tac,
@@ -2231,15 +2210,12 @@
             rtac (@{thm prop_subst} OF [surjective]),
             REPEAT o etac @{thm meta_allE}, atac]));
 
-    val split_meta_standard = timeit_msg ctxt "record split_meta standard:" (fn () =>
-      Drule.export_without_context split_meta);
-
     fun split_object_prf () =
       let
-        val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
-        val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
+        val cPI = cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
+        val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta));
         val cP = cterm_of defs_thy P;
-        val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;
+        val split_meta' = cterm_instantiate [(cP, cPI)] split_meta;
         val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
         val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
         val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
@@ -2258,7 +2234,7 @@
      in thr COMP (thl COMP iffI) end;
 
     val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
-      future_forward_prf split_object_prf split_object_prop);
+      future_forward_prf defs_thy split_object_prf split_object_prop);
 
     val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
       let
@@ -2267,19 +2243,17 @@
         val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
         val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
         val so'' = simplify ss so';
-      in
-        prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
-      end);
+      in prove [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end);
 
     fun equality_tac thms =
       let
         val s' :: s :: eqs = rev thms;
-        val ss' = ss addsimps (s' :: s :: sel_convs_standard);
+        val ss' = ss addsimps (s' :: s :: sel_convs);
         val eqs' = map (simplify ss') eqs;
       in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
 
     val equality = timeit_msg ctxt "record equality proof:" (fn () =>
-      prove_standard [] equality_prop (fn {context, ...} =>
+      prove [] [] equality_prop (fn {context, ...} =>
         fn st =>
           let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
             st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
@@ -2295,13 +2269,13 @@
           [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
       defs_thy
       |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
-         [("select_convs", sel_convs_standard),
-          ("update_convs", upd_convs_standard),
+         [("select_convs", sel_convs),
+          ("update_convs", upd_convs),
           ("select_defs", sel_defs),
           ("update_defs", upd_defs),
           ("fold_congs", fold_congs),
           ("unfold_congs", unfold_congs),
-          ("splits", [split_meta_standard, split_object, split_ex]),
+          ("splits", [split_meta, split_object, split_ex]),
           ("defs", derived_defs)]
       ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
           [("surjective", surjective),
@@ -2314,14 +2288,13 @@
 
     val sel_upd_simps = sel_convs' @ upd_convs';
     val sel_upd_defs = sel_defs' @ upd_defs';
-    val iffs = [ext_inject]
     val depth = parent_len + 1;
 
     val ([simps', iffs'], thms_thy') =
       thms_thy
       |> Global_Theory.add_thmss
           [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
-           ((Binding.name "iffs", iffs), [iff_add])];
+           ((Binding.name "iffs", [ext_inject]), [iff_add])];
 
     val info =
       make_info alphas parent fields extension