test/Tools/isac/Knowledge/diff.sml
changeset 52101 c3f399ce32af
parent 48790 98df8f6dc3f9
child 52142 e7febad0c988
     1.1 --- a/test/Tools/isac/Knowledge/diff.sml	Mon Sep 02 15:17:34 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Mon Sep 02 16:16:08 2013 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  val SOME (ctt,_) =
     1.5      (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
     1.6  "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----";
     1.7 -trace_rewrite := true;
     1.8 +trace_rewrite := false;
     1.9  val ct = "d_d s a";
    1.10      (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
    1.11  (*got: NONE instead SOME*)