# HG changeset patch
# User traytel
# Date 1348221067 -7200
# Node ID 394870e51d182075d59454896aaa6ab550579b02
# Parent  02eb071529986df6594d1fe3735d6c07c8a7e943
tuned antiquotations

diff -r 02eb07152998 -r 394870e51d18 src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 11:51:07 2012 +0200
@@ -56,7 +56,6 @@
 val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
 val ordIso_transitive = @{thm ordIso_transitive};
 val ordLeq_csum2 = @{thm ordLeq_csum2};
-val subset_UNIV = @{thm subset_UNIV};
 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
 val trans_o_apply = @{thm trans[OF o_apply]};
 
diff -r 02eb07152998 -r 394870e51d18 src/HOL/Codatatype/Tools/bnf_def_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 11:51:07 2012 +0200
@@ -36,7 +36,7 @@
 fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
 fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
 fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
-fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1
+fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
   else (rtac subsetI THEN'
   rtac CollectI) 1 THEN
   REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
@@ -107,8 +107,8 @@
   subst_tac ctxt [map_id] 1 THEN
     (if n = 0 then rtac refl 1
     else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
-      rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
-      CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
+      rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
+      CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
 
 fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
   unfold_defs_tac ctxt rel_O_Grs THEN
diff -r 02eb07152998 -r 394870e51d18 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 11:51:07 2012 +0200
@@ -205,7 +205,7 @@
     [etac @{thm UN_I}, atac]) 1;
 
 fun mk_set_incl_hin_tac incls =
-  if null incls then rtac @{thm subset_UNIV} 1
+  if null incls then rtac subset_UNIV 1
   else EVERY' [rtac subsetI, rtac CollectI,
     CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
 
@@ -534,7 +534,7 @@
         REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
         REPEAT_DETERM_N m o (rtac conjI THEN' atac),
         CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
-          rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order},
+          rtac subset_UNIV, rtac equalityD2, rtac @{thm Field_card_order},
           rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),
       atac] 1
   end;
@@ -1154,7 +1154,7 @@
         rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE},
         atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI,
         etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]},
-        rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
+        rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
         CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'),
           REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac])
         ks])
@@ -1377,7 +1377,7 @@
       SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI,
       REPEAT_DETERM o eresolve_tac [CollectE, conjE],
       rtac CollectI,
-      REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
+      REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
       CONJ_WRAP' (fn set_natural =>
         EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural,
           rtac trans_fun_cong_image_id_id_apply, atac])
diff -r 02eb07152998 -r 394870e51d18 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 11:51:07 2012 +0200
@@ -86,7 +86,6 @@
 val id_apply = @{thm id_apply};
 val meta_mp = @{thm meta_mp};
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val subset_UNIV = @{thm subset_UNIV};
 val subset_trans = @{thm subset_trans};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
 
diff -r 02eb07152998 -r 394870e51d18 src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 11:44:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 11:51:07 2012 +0200
@@ -123,6 +123,7 @@
   val o_apply: thm
   val set_mp: thm
   val set_rev_mp: thm
+  val subset_UNIV: thm
   val Pair_eqD: thm
   val Pair_eqI: thm
   val mk_sym: thm -> thm
@@ -524,6 +525,7 @@
 val o_apply = @{thm o_apply};
 val set_mp = @{thm set_mp};
 val set_rev_mp = @{thm set_rev_mp};
+val subset_UNIV = @{thm subset_UNIV};
 val Pair_eqD = @{thm iffD1[OF Pair_eq]};
 val Pair_eqI = @{thm iffD2[OF Pair_eq]};