changeset 61268 | abe08fb15a12 |
parent 61033 | fd7fe96ca7b9 |
child 66298 | 5ff9fe3fee66 |
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 20:37:59 2015 +0200 @@ -23,7 +23,7 @@ fun drop_fact_warning ctxt = SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o - Display.string_of_thm ctxt) + Thm.string_of_thm ctxt) (* general theorem normalizations *)