src/FOL/ex/Locale_Test/Locale_Test1.thy
changeset 37146 f652333bbf8e
parent 37134 29bd6c2ffba8
child 38108 b4115423c049
     1.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4  ML {*
     1.5    fun check_syntax ctxt thm expected =
     1.6      let
     1.7 -      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
     1.8 +      val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm;
     1.9      in
    1.10        if obtained <> expected
    1.11        then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")