src/Pure/meta_simplifier.ML
changeset 13569 69a6b3aa0f38
parent 13486 54464ea94d6f
child 13607 6908230623a3
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Sep 19 16:00:27 2002 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Sep 19 16:01:29 2002 +0200
     1.3 @@ -91,9 +91,12 @@
     1.4  fun trace_cterm warn a t = if !trace_simp then prctm warn a t else ();
     1.5  fun debug_term warn a sign t = if !debug_simp then prtm warn a sign t else ();
     1.6  
     1.7 -fun trace_thm warn a thm =
     1.8 +fun trace_thm a thm =
     1.9    let val {sign, prop, ...} = rep_thm thm
    1.10 -  in trace_term warn a sign prop end;
    1.11 +  in trace_term false a sign prop end;
    1.12 +
    1.13 +fun trace_named_thm a thm =
    1.14 +  trace_thm (a ^ " " ^ quote(Thm.name_of_thm thm) ^ ":") thm;
    1.15  
    1.16  end;
    1.17  
    1.18 @@ -233,7 +236,7 @@
    1.19  
    1.20  fun insert_rrule(mss as Mss {rules,...},
    1.21                   rrule as {thm,lhs,elhs,perm}) =
    1.22 -  (trace_thm false "Adding rewrite rule:" thm;
    1.23 +  (trace_named_thm "Adding rewrite rule" thm;
    1.24     let val rrule2 as {elhs,...} = mk_rrule2 rrule
    1.25         val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
    1.26     in upd_rules(mss,rules') end
    1.27 @@ -530,11 +533,11 @@
    1.28    let
    1.29      val thm'' = transitive thm (transitive
    1.30        (symmetric (beta_eta_conversion (lhs_of thm'))) thm')
    1.31 -  in (if msg then trace_thm false "SUCCEEDED" thm' else (); Some thm'') end
    1.32 +  in (if msg then trace_thm "SUCCEEDED" thm' else (); Some thm'') end
    1.33    handle THM _ =>
    1.34      let val {sign, prop = _ $ _ $ prop0, ...} = rep_thm thm;
    1.35      in
    1.36 -      (trace_thm false "Proved wrong thm (Check subgoaler?)" thm';
    1.37 +      (trace_thm "Proved wrong thm (Check subgoaler?)" thm';
    1.38         trace_term false "Should have proved:" sign prop0;
    1.39         None)
    1.40      end;
    1.41 @@ -612,19 +615,19 @@
    1.42          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
    1.43        in
    1.44          if perm andalso not (termless (rhs', lhs'))
    1.45 -        then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
    1.46 -              trace_thm false "Term does not become smaller:" thm'; None)
    1.47 -        else (trace_thm false "Applying instance of rewrite rule:" thm;
    1.48 +        then (trace_named_thm "Cannot apply permutative rewrite rule" thm;
    1.49 +              trace_thm "Term does not become smaller:" thm'; None)
    1.50 +        else (trace_named_thm "Applying instance of rewrite rule" thm;
    1.51             if unconditional
    1.52             then
    1.53 -             (trace_thm false "Rewriting:" thm';
    1.54 +             (trace_thm "Rewriting:" thm';
    1.55                let val lr = Logic.dest_equals prop;
    1.56                    val Some thm'' = check_conv false eta_thm thm'
    1.57                in Some (thm'', uncond_skel (congs, lr)) end)
    1.58             else
    1.59 -             (trace_thm false "Trying to rewrite:" thm';
    1.60 +             (trace_thm "Trying to rewrite:" thm';
    1.61                case prover (incr_depth mss) thm' of
    1.62 -                None       => (trace_thm false "FAILED" thm'; None)
    1.63 +                None       => (trace_thm "FAILED" thm'; None)
    1.64                | Some thm2 =>
    1.65                    (case check_conv true eta_thm thm2 of
    1.66                       None => None |
    1.67 @@ -657,7 +660,7 @@
    1.68                   (fn () => proc signt prems eta_t) () of
    1.69                 None => (debug false "FAILED"; proc_rews ps)
    1.70               | Some raw_thm =>
    1.71 -                 (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
    1.72 +                 (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
    1.73                    (case rews (mk_procrule raw_thm) of
    1.74                      None => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^
    1.75                        " -- does not match") t; proc_rews ps)
    1.76 @@ -684,7 +687,7 @@
    1.77        (* Pattern.match can raise Pattern.MATCH;
    1.78           is handled when congc is called *)
    1.79        val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
    1.80 -      val unit = trace_thm false "Applying congruence rule:" thm';
    1.81 +      val unit = trace_thm "Applying congruence rule:" thm';
    1.82        fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
    1.83    in case prover thm' of
    1.84         None => err ("Could not prove", thm')