changeset 26568 | 3a3a83493f00 |
parent 26291 | d01bf7b10c75 |
child 26626 | c6231d64d264 |
--- 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