--- a/src/HOL/Nominal/nominal_inductive.ML Mon Apr 07 15:37:34 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Apr 07 21:25:18 2008 +0200
@@ -27,7 +27,7 @@
(HOL_basic_ss addsimps inductive_atomize);
val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
- (Conv.forall_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
+ (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
val finite_Un = thm "finite_Un";
val supp_prod = thm "supp_prod";
--- a/src/Pure/Isar/object_logic.ML Mon Apr 07 15:37:34 2008 +0200
+++ b/src/Pure/Isar/object_logic.ML Mon Apr 07 21:25:18 2008 +0200
@@ -206,7 +206,7 @@
fun atomize_prems ct =
if Logic.has_meta_prems (Thm.term_of ct) then
- Conv.forall_conv ~1 (K (Conv.prems_conv ~1 atomize))
+ Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
(ProofContext.init (Thm.theory_of_cterm ct)) ct
else Conv.all_conv ct;
--- a/src/Tools/induct.ML Mon Apr 07 15:37:34 2008 +0200
+++ b/src/Tools/induct.ML Mon Apr 07 21:25:18 2008 +0200
@@ -528,7 +528,7 @@
end);
fun miniscope_tac p = CONVERSION o
- Conv.forall_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
+ Conv.params_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
in