tuned trace msgs;
authorwenzelm
Sat Apr 04 11:40:18 1998 +0200 (1998-04-04)
changeset 478552fa5258db2e
parent 4784 06556ca5036d
child 4786 9b6072bd71e4
tuned trace msgs;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri Apr 03 14:38:19 1998 +0200
     1.2 +++ b/src/Pure/thm.ML	Sat Apr 04 11:40:18 1998 +0200
     1.3 @@ -1576,7 +1576,7 @@
     1.4     let val rules' = Net.insert_term ((lhs, rrule), rules, eq_rrule)
     1.5     in upd_rules(mss,rules') end
     1.6     handle Net.INSERT =>
     1.7 -     (prthm true "Ignoring duplicate rewrite rule" thm; mss));
     1.8 +     (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
     1.9  
    1.10  fun vperm (Var _, Var _) = true
    1.11    | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    1.12 @@ -1691,7 +1691,7 @@
    1.13                rrule as {thm = thm, lhs = lhs, perm = perm}) =
    1.14    (upd_rules(mss, Net.delete_term ((lhs, rrule), rules, eq_rrule))
    1.15     handle Net.DELETE =>
    1.16 -     (prthm true "rewrite rule not in simpset" thm; mss));
    1.17 +     (prthm true "Rewrite rule not in simpset:" thm; mss));
    1.18  
    1.19  fun del_simps(mss,thms) =
    1.20    orient_comb_simps del_rrule (mk_rrule mss) (mss,thms);
    1.21 @@ -1739,7 +1739,7 @@
    1.22        (Sign.deref sign_ref) t;
    1.23      mk_mss (rules, congs,
    1.24        Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
    1.25 -        handle Net.INSERT => (trace true "ignored duplicate"; procs),
    1.26 +        handle Net.INSERT => (trace true "Ignored duplicate"; procs),
    1.27          bounds, prems, mk_rews, termless));
    1.28  
    1.29  fun add_simproc (mss, (name, lhss, proc, id)) =
    1.30 @@ -1754,7 +1754,7 @@
    1.31      (name, lhs as Cterm {t, ...}, proc, id)) =
    1.32    mk_mss (rules, congs,
    1.33      Net.delete_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
    1.34 -      handle Net.DELETE => (trace true "simplification procedure not in simpset"; procs),
    1.35 +      handle Net.DELETE => (trace true "Simplification procedure not in simpset"; procs),
    1.36        bounds, prems, mk_rews, termless);
    1.37  
    1.38  fun del_simproc (mss, (name, lhss, proc, id)) =
    1.39 @@ -1813,7 +1813,7 @@
    1.40  
    1.41  fun check_conv (thm as Thm{shyps,hyps,prop,sign_ref,der,...}, prop0, ders) =
    1.42    let fun err() = (trace_thm false "Proved wrong thm (Check subgoaler?)" thm;
    1.43 -                   trace_term false "Should have proved" (Sign.deref sign_ref) prop0;
    1.44 +                   trace_term false "Should have proved:" (Sign.deref sign_ref) prop0;
    1.45                     None)
    1.46        val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
    1.47    in case prop of
    1.48 @@ -1843,7 +1843,7 @@
    1.49  fun mk_procrule thm =
    1.50    let val (_,prems,lhs,rhs,_) = decomp_simp thm
    1.51    in if rewrite_rule_extra_vars prems lhs rhs
    1.52 -     then (prthm true "Extra vars on rhs" thm; [])
    1.53 +     then (prthm true "Extra vars on rhs:" thm; [])
    1.54       else [{thm = thm, lhs = lhs, perm = false}]
    1.55    end;
    1.56  
    1.57 @@ -1870,7 +1870,7 @@
    1.58      fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...}, lhs, perm} =
    1.59        let
    1.60          val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
    1.61 -                else (trace_thm true "rewrite rule from different theory" thm;
    1.62 +                else (trace_thm true "Rewrite rule from different theory:" thm;
    1.63                        raise Pattern.MATCH);
    1.64          val rprop = if maxt = ~1 then prop
    1.65                      else Logic.incr_indexes([],maxt+1) prop;
    1.66 @@ -1965,7 +1965,7 @@
    1.67                       hyps = union_term(hyps,hypst),
    1.68                       prop = prop',
    1.69                       maxidx = maxidx'};
    1.70 -      val unit = trace_thm false "Applying congruence rule" thm';
    1.71 +      val unit = trace_thm false "Applying congruence rule:" thm';
    1.72        fun err() = error("Failed congruence proof!")
    1.73  
    1.74    in case prover thm' of
    1.75 @@ -2093,7 +2093,7 @@
    1.76                             lhss1;
    1.77                in case dropwhile (not o reducible) prems of
    1.78                     [] => simpconc()
    1.79 -                 | red::rest => (trace_term false "Can now reduce premise" sg
    1.80 +                 | red::rest => (trace_term false "Can now reduce premise:" sg
    1.81                                              red;
    1.82                                   (Some(length rest,prem1),(conc,etc1)))
    1.83                end