# HG changeset patch
# User wenzelm
# Date 1207596318 -7200
# Node ID 3a3a83493f007afa3fe23f869c60e228f173982a
# Parent  7bcebb8c2d33dca43e684a348e310f0dc2a870c9
renamed iterated forall_conv to params_conv;

diff -r 7bcebb8c2d33 -r 3a3a83493f00 src/HOL/Nominal/nominal_inductive.ML
--- 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";
diff -r 7bcebb8c2d33 -r 3a3a83493f00 src/Pure/Isar/object_logic.ML
--- 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;
 
diff -r 7bcebb8c2d33 -r 3a3a83493f00 src/Tools/induct.ML
--- 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