1.1 --- a/src/Pure/thm.ML	Wed Aug 19 10:37:07 1998 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Aug 19 10:37:56 1998 +0200
     1.3 @@ -1889,7 +1889,7 @@
     1.4              lhs, elhs, fo, perm} =
     1.5        let
     1.6          val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
     1.7 -                else (trace_thm true "Rewrite rule from different theory:" thm;
     1.8 +                else (prthm true "Rewrite rule from different theory:" thm;
     1.9                        raise Pattern.MATCH);
    1.10          val rprop = if maxt = ~1 then prop
    1.11                      else Logic.incr_indexes([],maxt+1) prop;