1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -573,9 +573,9 @@
     1.4  	      (*"(?a | True) = True"*)
     1.5  	      Thm ("or_false",@{thm or_false}),
     1.6  	      (*"(?a | False) = ?a"*)
     1.7 -	      Thm ("not_true",num_str @{thm not_true}),
     1.8 +	      Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
     1.9  	      (*"(~ True) = False"*)
    1.10 -	      Thm ("not_false",num_str @{thm not_false})
    1.11 +	      Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
    1.12  	      (*"(~ False) = True"*)];
    1.13  (*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.14  val SOME (t', _) = rewrite_set_ thy false prls t;