full_rewrite_cterm_aux (see also tactic.ML);
no longer open MetaSimplifier;

--- a/src/Pure/meta_simplifier.ML	Thu Oct 04 15:21:17 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Oct 04 15:21:47 2001 +0200
@@ -1,13 +1,20 @@
 (*  Title:      Pure/meta_simplifier.ML
     ID:         $Id$
-    Author:     Tobias Nipkow
+    Author:     Tobias Nipkow and Stefan Berghofer
     Copyright   1994  University of Cambridge
 
-Meta Simplification
+Meta-level Simplification.
 *)
 
+signature BASIC_META_SIMPLIFIER =
+sig
+  val trace_simp: bool ref
+  val debug_simp: bool ref
+end;
+
 signature META_SIMPLIFIER =
 sig
+  include BASIC_META_SIMPLIFIER
   exception SIMPLIFIER of string * thm
   type meta_simpset
   val dest_mss		: meta_simpset ->
@@ -32,11 +39,9 @@
   val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
   val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
-  val trace_simp        : bool ref
-  val debug_simp        : bool ref
-  val rewrite_cterm     : bool * bool * bool
-                          -> (meta_simpset -> thm -> thm option)
-                          -> meta_simpset -> cterm -> thm
+  val rewrite_cterm: bool * bool * bool ->
+    (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> 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
                           -> (meta_simpset -> thm -> thm option)
@@ -931,6 +936,12 @@
 (*Use a conversion to transform a theorem*)
 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
 
+(*Rewrite a cterm (yielding again a cterm instead of a theorem)*)
+fun full_rewrite_cterm_aux _ [] = (fn ct => ct)
+  | full_rewrite_cterm_aux prover thms =
+      #2 o Thm.dest_comb o #prop o Thm.crep_thm o
+        rewrite_cterm (true, false, false) prover (mss_of thms);
+
 (*Rewrite a theorem*)
 fun rewrite_rule_aux _ [] = (fn th => th)
   | rewrite_rule_aux prover thms =
@@ -952,4 +963,5 @@
 
 end;
 
-open MetaSimplifier;
+structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
+open BasicMetaSimplifier;