src/Pure/meta_simplifier.ML

 signature META_SIMPLIFIER =
 sig
   include BASIC_META_SIMPLIFIER
   exception SIMPLIFIER of string * thm
   type meta_simpset
-  val dest_mss		: meta_simpset ->
+  val dest_mss          : meta_simpset ->
     {simps: thm list, congs: thm list, procs: (string * cterm list) list}
   val empty_mss         : meta_simpset
-  val clear_mss		: meta_simpset -> meta_simpset
-  val merge_mss		: meta_simpset * meta_simpset -> meta_simpset
+  val clear_mss         : meta_simpset -> meta_simpset
+  val merge_mss         : meta_simpset * meta_simpset -> meta_simpset
   val add_simps         : meta_simpset * thm list -> meta_simpset
   val del_simps         : meta_simpset * thm list -> meta_simpset
   val mss_of            : thm list -> meta_simpset
   val add_congs         : meta_simpset * thm list -> meta_simpset
   val del_congs         : meta_simpset * thm list -> meta_simpset
-  val add_simprocs	: meta_simpset *
+  val add_simprocs      : meta_simpset *
     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
       -> meta_simpset
-  val del_simprocs	: meta_simpset *
+  val del_simprocs      : meta_simpset *
     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
       -> meta_simpset
   val add_prems         : meta_simpset * thm list -> meta_simpset
   val prems_of_mss      : meta_simpset -> thm list
   val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset

 
 exception SIMPLIFIER of string * thm;
 
 val simp_depth = ref 0;
 
-fun println a = tracing (replicate_string (! simp_depth) " " ^ a);
+local
+
+fun println a =
+  tracing ((case ! simp_depth of 0 => "" | n => "[" ^ string_of_int n ^ "]") ^ a);
 
 fun prnt warn a = if warn then warning a else println a;
-
-fun prtm warn a sign t =
-  (prnt warn a; prnt warn (Sign.string_of_term sign t));
-
-fun prctm warn a t =
-  (prnt warn a; prnt warn (Display.string_of_cterm t));
-
-fun prthm warn a thm =
-  let val {sign, prop, ...} = rep_thm thm
-  in prtm warn a sign prop end;
+fun prtm warn a sign t = prnt warn (a ^ "\n" ^ Sign.string_of_term sign t);
+fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
+
+in
+
+fun prthm warn a = prctm warn a o Thm.cprop_of;
 
 val trace_simp = ref false;
 val debug_simp = ref false;
 
 fun trace warn a = if !trace_simp then prnt warn a else ();

 
 fun trace_thm warn a thm =
   let val {sign, prop, ...} = rep_thm thm
   in trace_term warn a sign prop end;
 
+end;
 
 
 (** meta simp sets **)
 
 (* basic components *)

 (* thm: the rewrite rule
    lhs: the left-hand side
    elhs: the etac-contracted lhs.
    fo:  use first-order matching
    perm: the rewrite rule is permutative
-Reamrks:
+Remarks:
   - elhs is used for matching,
     lhs only for preservation of bound variable names.
   - fo is set iff
     either elhs is first-order (no Var is applied),
            in which case fo-matching is complete,

  {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
 
 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
   #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
 
-fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) = 
+fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
   #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
 
 fun eq_prem (thm1, thm2) =
   #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
 

 fun clear_mss (Mss {mk_rews, termless, ...}) =
   mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless,0);
 
 fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) =
   mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth+1)
- 
+
 
 
 (** simpset operations **)
 
 (* term variables *)

      |> partition_eq eq_snd
      |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
      |> Library.sort_wrt #1};
 
 
-(* merge_mss *)	      (*NOTE: ignores mk_rews, termless and depth of 2nd mss*)
+(* merge_mss *)       (*NOTE: ignores mk_rews, termless and depth of 2nd mss*)
 
 fun merge_mss
  (Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
        bounds = bounds1, prems = prems1, mk_rews, termless, depth},
   Mss {rules = rules2, congs = (congs2,weak2), procs = procs2,

   let val {sign, t, ...} = rep_cterm lhs
   in (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
       sign t;
     mk_mss (rules, congs,
       Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
-        handle Net.INSERT => 
-	    (warning ("Ignoring duplicate simplification procedure \"" 
-	              ^ name ^ "\""); 
-	     procs),
+        handle Net.INSERT =>
+            (warning ("Ignoring duplicate simplification procedure \""
+                      ^ name ^ "\"");
+             procs),
         bounds, prems, mk_rews, termless,depth))
   end;
 
 fun add_simproc (mss, (name, lhss, proc, id)) =
   foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);

 
 fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth},
     (name, lhs, proc, id)) =
   mk_mss (rules, congs,
     Net.delete_term ((term_of lhs, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
-      handle Net.DELETE => 
-	  (warning ("Simplification procedure \"" ^ name ^
-		       "\" not in simpset"); procs),
+      handle Net.DELETE =>
+          (warning ("Simplification procedure \"" ^ name ^
+                       "\" not in simpset"); procs),
       bounds, prems, mk_rews, termless, depth);
 
 fun del_simproc (mss, (name, lhss, proc, id)) =
   foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
 

       | rews (rrule :: rrules) =
           let val opt = rew rrule handle Pattern.MATCH => None
           in case opt of None => rews rrules | some => some end;
 
     fun sort_rrules rrs = let
-      fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of 
+      fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
                                       Const("==",_) $ _ $ _ => true
-                                      | _                   => false 
+                                      | _                   => false
       fun sort []        (re1,re2) = re1 @ re2
-        | sort (rr::rrs) (re1,re2) = if is_simple rr 
+        | sort (rr::rrs) (re1,re2) = if is_simple rr
                                      then sort rrs (rr::re1,re2)
                                      else sort rrs (re1,rr::re2)
     in sort rrs ([],[]) end
 
     fun proc_rews ([]:simproc list) = None

           end
 
         fun rebuild None = (case rewritec (prover, sign, maxidx) mss
             (mk_implies (prem1, conc)) of
               None => None
-            | Some (thm, _) => 
+            | Some (thm, _) =>
                 let val (prem, conc) = Drule.dest_implies (rhs_of thm)
                 in (case mut_impc (prems, prem, conc, mss) of
                     None => Some (None, thm)
                   | Some (x, thm') => Some (x, transitive thm thm'))
                 end handle TERM _ => Some (None, thm))