--- a/src/HOL/Tools/record.ML Wed Jan 11 16:23:59 2012 +0100
+++ b/src/HOL/Tools/record.ML Wed Jan 11 16:25:34 2012 +0100
@@ -1630,7 +1630,7 @@
Skip_Proof.prove_global defs_thy [] [] split_meta_prop
(fn _ =>
EVERY1
- [rtac equal_intr_rule, Goal.norm_hhf_tac,
+ [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
etac @{thm meta_allE}, atac,
rtac (@{thm prop_subst} OF [surject]),
REPEAT o etac @{thm meta_allE}, atac]));
@@ -2155,7 +2155,7 @@
Skip_Proof.prove_global defs_thy [] [] split_meta_prop
(fn _ =>
EVERY1
- [rtac equal_intr_rule, Goal.norm_hhf_tac,
+ [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
etac @{thm meta_allE}, atac,
rtac (@{thm prop_subst} OF [surjective]),
REPEAT o etac @{thm meta_allE}, atac]));
--- a/src/Pure/drule.ML Wed Jan 11 16:23:59 2012 +0100
+++ b/src/Pure/drule.ML Wed Jan 11 16:25:34 2012 +0100
@@ -41,26 +41,17 @@
val COMP: thm * thm -> thm
val INCR_COMP: thm * thm -> thm
val COMP_INCR: thm * thm -> thm
- val cterm_instantiate: (cterm*cterm)list -> thm -> thm
+ val cterm_instantiate: (cterm * cterm) list -> thm -> thm
val size_of_thm: thm -> int
val reflexive_thm: thm
val symmetric_thm: thm
val transitive_thm: thm
val symmetric_fun: thm -> thm
val extensional: thm -> thm
- val equals_cong: thm
- val imp_cong: thm
- val swap_prems_eq: thm
val asm_rl: thm
val cut_rl: thm
val revcut_rl: thm
val thin_rl: thm
- val triv_forall_equality: thm
- val distinct_prems_rl: thm
- val swap_prems_rl: thm
- val equal_intr_rule: thm
- val equal_elim_rule1: thm
- val equal_elim_rule2: thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
end;
@@ -81,6 +72,9 @@
val store_thm_open: binding -> thm -> thm
val store_standard_thm_open: binding -> thm -> thm
val compose_single: thm * int * thm -> thm
+ val equals_cong: thm
+ val imp_cong: thm
+ val swap_prems_eq: thm
val imp_cong_rule: thm -> thm -> thm
val arg_cong_rule: cterm -> thm -> thm
val binop_cong_rule: cterm -> thm -> thm -> thm
@@ -112,6 +106,12 @@
val rename_bvars': string option list -> thm -> thm
val incr_indexes: thm -> thm -> thm
val incr_indexes2: thm -> thm -> thm -> thm
+ val triv_forall_equality: thm
+ val distinct_prems_rl: thm
+ val swap_prems_rl: thm
+ val equal_intr_rule: thm
+ val equal_elim_rule1: thm
+ val equal_elim_rule2: thm
val remdups_rl: thm
val multi_resolve: thm list -> thm -> thm Seq.seq
val multi_resolves: thm list -> thm list -> thm Seq.seq
--- a/src/Pure/raw_simplifier.ML Wed Jan 11 16:23:59 2012 +0100
+++ b/src/Pure/raw_simplifier.ML Wed Jan 11 16:25:34 2012 +0100
@@ -1322,7 +1322,7 @@
(*Prunes all redundant parameters from the proof state by rewriting.
DOES NOT rewrite main goal, where quantification over an unused bound
variable is sometimes done to avoid the need for cut_facts_tac.*)
-val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
+val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
(* for folding definitions, handling critical pairs *)
--- a/src/Sequents/simpdata.ML Wed Jan 11 16:23:59 2012 +0100
+++ b/src/Sequents/simpdata.ML Wed Jan 11 16:25:34 2012 +0100
@@ -75,7 +75,7 @@
|> Simplifier.set_mkcong mk_meta_cong;
val LK_simps =
- [triv_forall_equality, (* prunes params *)
+ [@{thm triv_forall_equality}, (* prunes params *)
@{thm refl} RS @{thm P_iff_T}] @
@{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @
@{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @
--- a/src/Tools/coherent.ML Wed Jan 11 16:23:59 2012 +0100
+++ b/src/Tools/coherent.ML Wed Jan 11 16:25:34 2012 +0100
@@ -209,7 +209,7 @@
(** external interface **)
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
- rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
+ rtac (rulify_elim_conv concl RS Drule.equal_elim_rule2) 1 THEN
SUBPROOF (fn {prems = prems', concl, context, ...} =>
let val xs = map (term_of o #2) params @
map (fn (_, s) => Free (s, the (Variable.default_type context s)))