# HG changeset patch
# User wenzelm
# Date 1326295534 -3600
# Node ID 9ae331a1d8c55297ff7bd0c5cdb6c5002c5622a6
# Parent  afda84cd4d4b36b5b0d4fae7519222fc31f3c33b
more qualified names;
more antiquotations;

diff -r afda84cd4d4b -r 9ae331a1d8c5 src/HOL/Tools/record.ML
--- 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]));
diff -r afda84cd4d4b -r 9ae331a1d8c5 src/Pure/drule.ML
--- 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
diff -r afda84cd4d4b -r 9ae331a1d8c5 src/Pure/raw_simplifier.ML
--- 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 *)
diff -r afda84cd4d4b -r 9ae331a1d8c5 src/Sequents/simpdata.ML
--- 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} @
diff -r afda84cd4d4b -r 9ae331a1d8c5 src/Tools/coherent.ML
--- 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)))