1.1 --- a/src/HOL/Tools/record.ML	Fri Dec 30 13:52:07 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Dec 30 14:19:58 2011 +0100
     1.3 @@ -949,14 +949,6 @@
     1.4  
     1.5  (** record simprocs **)
     1.6  
     1.7 -fun future_forward_prf thy prf prop =
     1.8 -  let val thm =
     1.9 -    if ! quick_and_dirty then Skip_Proof.make_thm thy prop
    1.10 -    else if Goal.future_enabled () then
    1.11 -      Goal.future_result (Proof_Context.init_global thy) (Goal.fork prf) prop
    1.12 -    else prf ()
    1.13 -  in Drule.export_without_context thm end;
    1.14 -
    1.15  fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
    1.16    (case get_updates thy u of
    1.17      SOME u_name => u_name = s
    1.18 @@ -2065,8 +2057,7 @@
    1.19  
    1.20      (*cases*)
    1.21      val cases_scheme_prop =
    1.22 -      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
    1.23 -        ==> Trueprop C;
    1.24 +      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
    1.25  
    1.26      val cases_prop =
    1.27        (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
    1.28 @@ -2128,31 +2119,10 @@
    1.29              asm_simp_tac HOL_basic_ss 1]));
    1.30  
    1.31      val induct = timeit_msg ctxt "record induct proof:" (fn () =>
    1.32 -      let val (assm, concl) = induct_prop in
    1.33 -        Skip_Proof.prove_global defs_thy [] [assm] concl (fn {prems, ...} =>
    1.34 -          try_param_tac rN induct_scheme 1
    1.35 -          THEN try_param_tac "more" @{thm unit.induct} 1
    1.36 -          THEN resolve_tac prems 1)
    1.37 -      end);
    1.38 -
    1.39 -    fun cases_scheme_prf () =
    1.40 -      let
    1.41 -        val _ $ (Pvar $ _) = concl_of induct_scheme;
    1.42 -        val ind =
    1.43 -          cterm_instantiate
    1.44 -            [(cterm_of defs_thy Pvar, cterm_of defs_thy
    1.45 -              (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
    1.46 -            induct_scheme;
    1.47 -        in Object_Logic.rulify (mp OF [ind, refl]) end;
    1.48 -
    1.49 -    val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
    1.50 -      future_forward_prf defs_thy cases_scheme_prf cases_scheme_prop);
    1.51 -
    1.52 -    val cases = timeit_msg ctxt "record cases proof:" (fn () =>
    1.53 -      Skip_Proof.prove_global defs_thy [] [] cases_prop
    1.54 -        (fn _ =>
    1.55 -          try_param_tac rN cases_scheme 1 THEN
    1.56 -          ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps [@{thm unit_all_eq1}]))));
    1.57 +      Skip_Proof.prove_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
    1.58 +        try_param_tac rN induct_scheme 1
    1.59 +        THEN try_param_tac "more" @{thm unit.induct} 1
    1.60 +        THEN resolve_tac prems 1));
    1.61  
    1.62      val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
    1.63        let
    1.64 @@ -2170,6 +2140,18 @@
    1.65                    (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
    1.66        end);
    1.67  
    1.68 +    val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
    1.69 +      Skip_Proof.prove_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
    1.70 +        (fn {prems, ...} =>
    1.71 +          resolve_tac prems 1 THEN
    1.72 +          rtac surjective 1));
    1.73 +
    1.74 +    val cases = timeit_msg ctxt "record cases proof:" (fn () =>
    1.75 +      Skip_Proof.prove_global defs_thy [] [] cases_prop
    1.76 +        (fn _ =>
    1.77 +          try_param_tac rN cases_scheme 1 THEN
    1.78 +          ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps @{thms unit_all_eq1}))));
    1.79 +
    1.80      val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
    1.81        Skip_Proof.prove_global defs_thy [] [] split_meta_prop
    1.82          (fn _ =>