# 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;