--- a/src/HOL/Code_Generator.thy Wed May 09 23:28:18 2007 +0200
+++ b/src/HOL/Code_Generator.thy Thu May 10 00:39:45 2007 +0200
@@ -73,8 +73,8 @@
method_setup evaluation = {*
let
-fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
- (Drule.goals_conv (equal i) Codegen.evaluation_conv));
+fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
+ (Conv.goals_conv (equal i) Codegen.evaluation_conv));
in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
*} "solve goal by evaluation"
@@ -201,8 +201,8 @@
method_setup normalization = {*
let
- fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
- (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv
+ fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
+ (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
NBE.normalization_conv)));
in
Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
--- a/src/HOL/Library/EfficientNat.thy Wed May 09 23:28:18 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy Thu May 10 00:39:45 2007 +0200
@@ -290,7 +290,7 @@
let
val th' =
Thm.implies_elim
- (Drule.fconv_rule (Thm.beta_conversion true)
+ (Conv.fconv_rule (Thm.beta_conversion true)
(Drule.instantiate'
[SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
@@ -338,7 +338,7 @@
let
val cert = cterm_of (Thm.theory_of_thm th);
val th'' = ObjectLogic.rulify (Thm.implies_elim
- (Drule.fconv_rule (Thm.beta_conversion true)
+ (Conv.fconv_rule (Thm.beta_conversion true)
(Drule.instantiate' []
[SOME (cert (lambda v (Abs ("x", HOLogic.natT,
abstract_over (Sucv,
--- a/src/HOL/Tools/sat_funcs.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Thu May 10 00:39:45 2007 +0200
@@ -434,7 +434,7 @@
fun pre_cnf_tac i =
rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
- PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion)));
+ PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (Drule.beta_eta_conversion)));
(* ------------------------------------------------------------------------- *)
(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
--- a/src/HOL/arith_data.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/HOL/arith_data.ML Thu May 10 00:39:45 2007 +0200
@@ -896,8 +896,8 @@
(TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
THEN_ALL_NEW
((fn j => PRIMITIVE
- (Drule.fconv_rule
- (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
+ (Conv.fconv_rule
+ (Conv.goals_conv (equal j) (Drule.beta_eta_conversion))))
THEN'
(TRY o (etac notE THEN' eq_assume_tac)))
) i
--- a/src/Provers/induct_method.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/Provers/induct_method.ML Thu May 10 00:39:45 2007 +0200
@@ -195,7 +195,7 @@
fun internalize k th =
th |> Thm.permute_prems 0 k
- |> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th - k) atomize_cterm);
+ |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
(* guess rule instantiation -- cannot handle pending goal parameters *)
@@ -310,9 +310,9 @@
| NONE => all_tac)
end);
-fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
- (Drule.goals_conv (Library.equal i)
- (Drule.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
+fun miniscope_tac p i = PRIMITIVE (Conv.fconv_rule
+ (Conv.goals_conv (Library.equal i)
+ (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
in
--- a/src/Pure/Isar/attrib.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/Pure/Isar/attrib.ML Thu May 10 00:39:45 2007 +0200
@@ -252,7 +252,8 @@
let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt)
in th' end)) x;
-fun eta_long x = no_args (Thm.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x;
+fun eta_long x =
+ no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion))) x;
(* internal attribute *)
--- a/src/Pure/Isar/element.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/Pure/Isar/element.ML Thu May 10 00:39:45 2007 +0200
@@ -456,7 +456,7 @@
else th |> hyps_rule
(instantiate_tfrees thy substT #>
instantiate_frees thy subst #>
- Drule.fconv_rule (Thm.beta_conversion true))
+ Conv.fconv_rule (Thm.beta_conversion true))
end;
fun inst_morphism thy envs =
--- a/src/Pure/Isar/local_defs.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML Thu May 10 00:39:45 2007 +0200
@@ -171,10 +171,10 @@
MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
(equals_ss addsimps (Rules.get (Context.Proof ctxt)));
-val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite;
+val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite;
fun meta_rewrite_tac ctxt i =
- PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt)));
+ PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (meta_rewrite ctxt)));
(* rewriting with object-level rules *)
--- a/src/Pure/Isar/object_logic.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML Thu May 10 00:39:45 2007 +0200
@@ -141,10 +141,10 @@
(* atomize *)
-fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule
- (Drule.goals_conv (Library.equal i)
- (Drule.forall_conv ~1
- (Drule.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
+fun rewrite_prems_tac rews i = PRIMITIVE (Conv.fconv_rule
+ (Conv.goals_conv (Library.equal i)
+ (Conv.forall_conv ~1
+ (Conv.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
fun atomize_term thy =
drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
--- a/src/Pure/Isar/rule_cases.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML Thu May 10 00:39:45 2007 +0200
@@ -189,14 +189,14 @@
fun unfold_prems n defs th =
if null defs then th
- else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
+ else Conv.fconv_rule (Conv.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
fun unfold_prems_concls defs th =
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
else
- Drule.fconv_rule
- (Drule.concl_conv ~1 (Conjunction.conv ~1
- (K (Drule.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
+ Conv.fconv_rule
+ (Conv.concl_conv ~1 (Conjunction.conv ~1
+ (K (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
in
--- a/src/Pure/Tools/codegen_func.ML Wed May 09 23:28:18 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML Thu May 10 00:39:45 2007 +0200
@@ -109,7 +109,7 @@
val _ = map (check 0) args;
in thm end;
-val mk_func = assert_func o Drule.fconv_rule Drule.beta_eta_conversion o mk_rew;
+val mk_func = assert_func o Conv.fconv_rule Drule.beta_eta_conversion o mk_rew;
fun head_func thm =
let
@@ -183,7 +183,7 @@
in
thms
|> map (expand_eta k)
- |> map (Drule.fconv_rule Drule.beta_eta_conversion)
+ |> map (Conv.fconv_rule Drule.beta_eta_conversion)
end;
fun canonical_tvars purify_tvar thm =