src/Pure/meta_simplifier.ML

   exception SIMPROC_FAIL of string * exn
   val simproc_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
-  val revert_bound: simpset -> string -> string option
   val inherit_bounds: simpset -> simpset -> simpset
   val rewrite_cterm: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> cterm -> thm
   val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
   val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm

     val used = Term.add_term_names (t, []);
     val xs = rev (Term.variantlist (rev (map #2 bs), used));
     fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
 
-fun prtm warn a ss thy t = prnt warn (a ^ "\n" ^
+in
+
+fun print_term warn a ss thy t = prnt warn (a ^ "\n" ^
   Sign.string_of_term thy (if ! debug_simp then t else show_bounds ss t));
-
-in
 
 fun debug warn a = if ! debug_simp then prnt warn a else ();
 fun trace warn a = if ! trace_simp then prnt warn a else ();
 
-fun debug_term warn a ss thy t = if ! debug_simp then prtm warn a ss thy t else ();
-fun trace_term warn a ss thy t = if ! trace_simp then prtm warn a ss thy t else ();
+fun debug_term warn a ss thy t = if ! debug_simp then print_term warn a ss thy t else ();
+fun trace_term warn a ss thy t = if ! trace_simp then print_term warn a ss thy t else ();
 
 fun trace_cterm warn a ss ct =
-  if ! trace_simp then prtm warn a ss (Thm.theory_of_cterm ct) (Thm.term_of ct) else ();
+  if ! trace_simp then print_term warn a ss (Thm.theory_of_cterm ct) (Thm.term_of ct) else ();
 
 fun trace_thm a ss th =
-  if ! trace_simp then prtm false a ss (Thm.theory_of_thm th) (Thm.full_prop_of th) else ();
+  if ! trace_simp then print_term false a ss (Thm.theory_of_thm th) (Thm.full_prop_of th) else ();
 
 fun trace_named_thm a ss (th, name) =
   if ! trace_simp then
-    prtm false (if name = "" then a else a ^ " " ^ quote name ^ ":") ss
+    print_term false (if name = "" then a else a ^ " " ^ quote name ^ ":") ss
       (Thm.theory_of_thm th) (Thm.full_prop_of th)
   else ();
 
-fun warn_thm a ss th = prtm true a ss (Thm.theory_of_thm th) (Thm.full_prop_of th);
+fun warn_thm a ss th = print_term true a ss (Thm.theory_of_thm th) (Thm.full_prop_of th);
 
 end;
 
 
 (* print simpsets *)

 (** simpset operations **)
 
 (* bounds and prems *)
 
 fun eq_bound (x: string, (y, _)) = x = y;
-
-fun revert_bound (Simpset ({bounds = (_, bs), ...}, _)) = AList.lookup eq_bound bs;
 
 fun inherit_bounds (Simpset ({bounds, ...}, _)) =
   map_simpset1 (fn (rules, prems, _) => (rules, prems, bounds));
 
 fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds)) =>

             use prems of B (if B is again a meta-impl.) to simplify A)
            when simplifying A ==> B
     prover: how to solve premises in conditional rewrites and congruences
 *)
 
-fun check_bounds ss ct = conditional (! debug_simp) (fn () =>
+val debug_bounds = ref false;
+
+fun check_bounds ss ct = conditional (! debug_bounds) (fn () =>
   let
     val Simpset ({bounds = (_, bounds), ...}, _) = ss;
     val bs = fold_aterms (fn Free (x, _) =>
         if Term.is_bound x andalso not (AList.defined eq_bound bounds x)
         then insert (op =) x else I
       | _ => I) (term_of ct) [];
-  in if null bs then () else warning ("Simplifier: term contains loose bounds: " ^ commas bs) end);
+  in
+    if null bs then ()
+    else print_term true ("Simplifier: term contains loose bounds: " ^ commas bs) ss
+      (Thm.theory_of_cterm ct) (Thm.term_of ct)
+  end);
 
 fun rewrite_cterm mode prover ss ct =
   (inc simp_depth;
    if !simp_depth mod 20 = 0
    then warning ("Simplification depth " ^ string_of_int (!simp_depth))