1.1 --- a/src/HOL/Tools/record.ML	Fri Dec 30 12:12:16 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Dec 30 12:54:55 2011 +0100
     1.3 @@ -1477,8 +1477,7 @@
     1.4      val params = Logic.strip_params g;
     1.5      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
     1.6      val rule' = Thm.lift_rule cgoal rule;
     1.7 -    val (P, ys) = strip_comb (HOLogic.dest_Trueprop
     1.8 -      (Logic.strip_assums_concl (prop_of rule')));
     1.9 +    val (P, ys) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (prop_of rule')));
    1.10      (*ca indicates if rule is a case analysis or induction rule*)
    1.11      val (x, ca) =
    1.12        (case rev (drop (length params) ys) of
    1.13 @@ -1688,27 +1687,6 @@
    1.14    fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
    1.15  
    1.16  
    1.17 -fun obj_to_meta_all thm =
    1.18 -  let
    1.19 -    fun E thm =  (* FIXME proper name *)
    1.20 -      (case SOME (spec OF [thm]) handle THM _ => NONE of
    1.21 -        SOME thm' => E thm'
    1.22 -      | NONE => thm);
    1.23 -    val th1 = E thm;
    1.24 -    val th2 = Drule.forall_intr_vars th1;
    1.25 -  in th2 end;
    1.26 -
    1.27 -fun meta_to_obj_all thm =
    1.28 -  let
    1.29 -    val thy = Thm.theory_of_thm thm;
    1.30 -    val prop = Thm.prop_of thm;
    1.31 -    val params = Logic.strip_params prop;
    1.32 -    val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
    1.33 -    val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
    1.34 -    val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
    1.35 -  in Thm.implies_elim thm' thm end;
    1.36 -
    1.37 -
    1.38  (* code generation *)
    1.39  
    1.40  fun mk_random_eq tyco vs extN Ts =
    1.41 @@ -2201,31 +2179,12 @@
    1.42              rtac (@{thm prop_subst} OF [surjective]),
    1.43              REPEAT o etac @{thm meta_allE}, atac]));
    1.44  
    1.45 -    fun split_object_prf () =
    1.46 -      let
    1.47 -        val cPI = cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
    1.48 -        val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta));
    1.49 -        val cP = cterm_of defs_thy P;
    1.50 -        val split_meta' = cterm_instantiate [(cP, cPI)] split_meta;
    1.51 -        val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
    1.52 -        val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
    1.53 -        val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
    1.54 -        val thl =
    1.55 -          Thm.assume cl                   (*All r. P r*) (* 1 *)
    1.56 -          |> obj_to_meta_all              (*!!r. P r*)
    1.57 -          |> Thm.equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
    1.58 -          |> meta_to_obj_all              (*All n m more. P (ext n m more)*) (* 2*)
    1.59 -          |> Thm.implies_intr cl          (* 1 ==> 2 *)
    1.60 -        val thr =
    1.61 -          Thm.assume cr                                 (*All n m more. P (ext n m more)*)
    1.62 -          |> obj_to_meta_all                            (*!!n m more. P (ext n m more)*)
    1.63 -          |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
    1.64 -          |> meta_to_obj_all                            (*All r. P r*)
    1.65 -          |> Thm.implies_intr cr                        (* 2 ==> 1 *)
    1.66 -     in thr COMP (thl COMP iffI) end;
    1.67 -
    1.68      val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
    1.69 -      future_forward_prf defs_thy split_object_prf split_object_prop);
    1.70 +      Skip_Proof.prove_global defs_thy [] [] split_object_prop
    1.71 +        (fn _ =>
    1.72 +          rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
    1.73 +          rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
    1.74 +          rtac split_meta 1));
    1.75  
    1.76      val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
    1.77        let