# HG changeset patch
# User berghofe
# Date 1002898627 -7200
# Node ID da6fc37ed6fa34f0b5119417c0f7f28fc4c881ba
# Parent  60c0fa10bfc2cd929aea95b3f1fd36a85293b6d8
- Exported goals_conv and fconv_rule
- Added forall_conv

diff -r 60c0fa10bfc2 -r da6fc37ed6fa src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Oct 12 12:13:31 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Oct 12 16:57:07 2001 +0200
@@ -41,6 +41,9 @@
   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
   val rewrite_cterm: bool * bool * bool ->
     (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
+  val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
+  val forall_conv       : (cterm -> thm) -> cterm -> thm
+  val fconv_rule        : (cterm -> thm) -> thm -> thm
   val full_rewrite_cterm_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> cterm
   val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_thm       : bool * bool * bool
@@ -931,6 +934,18 @@
         handle TERM _ => reflexive ct
   in gconv 1 end;
 
+(* Rewrite A in !!x1,...x1. A *)
+fun forall_conv cv ct =
+  let val p as (ct1, ct2) = Thm.dest_comb ct
+  in (case pairself term_of p of
+      (Const ("all", _), Abs (s, _, _)) =>
+         let val (v, ct') = Thm.dest_abs (Some "@") ct2;
+         in Thm.combination (Thm.reflexive ct1)
+           (Thm.abstract_rule s v (forall_conv cv ct'))
+         end
+    | _ => cv ct)
+  end handle TERM _ => cv ct;
+
 (*Use a conversion to transform a theorem*)
 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;