# HG changeset patch
# User wenzelm
# Date 1129911280 -7200
# Node ID 5662fa033a9252529e9f87a9b75096a36c314371
# Parent  8db36a1082132c871d20a93f3826f73fb662e7a7
avoid triv_goal and home-grown meta_allE;

diff -r 8db36a108213 -r 5662fa033a92 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Oct 21 18:14:38 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Oct 21 18:14:40 2005 +0200
@@ -43,7 +43,7 @@
 end;
 
 
-structure RecordPackage:RECORD_PACKAGE =
+structure RecordPackage: RECORD_PACKAGE =
 struct
 
 val rec_UNIV_I = thm "rec_UNIV_I";
@@ -51,8 +51,8 @@
 val Pair_eq = thm "Product_Type.Pair_eq";
 val atomize_all = thm "HOL.atomize_all";
 val atomize_imp = thm "HOL.atomize_imp";
-val triv_goal   = thm "triv_goal";
-val prop_subst  = thm "prop_subst";
+val meta_allE = thm "Pure.meta_allE";
+val prop_subst = thm "prop_subst";
 val Pair_sel_convs = [fst_conv,snd_conv];
 
 
@@ -800,11 +800,11 @@
 
 fun quick_and_dirty_prove stndrd sg asms prop tac =
   if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
-  then Tactic.prove sg [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
+  then Goal.prove sg [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
         (K (SkipProof.cheat_tac HOL.thy))
         (* standard can take quite a while for large records, thats why
          * we varify the proposition manually here.*)
-  else let val prf = Tactic.prove sg [] asms prop tac;
+  else let val prf = Goal.prove sg [] asms prop tac;
        in if stndrd then standard prf else prf end;
 
 fun quick_and_dirty_prf noopt opt () =
@@ -1494,11 +1494,10 @@
 
     fun split_meta_prf () =
         prove_standard [] split_meta_prop (fn prems =>
-         EVERY [rtac equal_intr_rule 1,
-                  rtac meta_allE 1, etac triv_goal 1, atac 1,
+         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
+                etac meta_allE 1, atac 1,
                 rtac (prop_subst OF [surjective]) 1,
-                REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
-                atac 1]);
+                REPEAT (etac meta_allE 1), atac 1]);
     val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
 
     val (thm_thy,([inject',induct',cases',surjective',split_meta'],
@@ -1901,11 +1900,10 @@
 
     fun split_meta_prf () =
         prove false [] split_meta_prop (fn prems =>
-         EVERY [rtac equal_intr_rule 1,
-                  rtac meta_allE 1, etac triv_goal 1, atac 1,
+         EVERY [rtac equal_intr_rule 1, norm_hhf_tac 1,
+                etac meta_allE 1, atac 1,
                 rtac (prop_subst OF [surjective]) 1,
-                REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
-                atac 1]);
+                REPEAT (etac meta_allE 1), atac 1]);
     val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
     val split_meta_standard = standard split_meta;