src/HOL/Import/shuffler.ML
changeset 37146 f652333bbf8e
parent 36945 9bec62c10714
child 37778 87b5dfe00387
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  (*Prints an exception, then fails*)
     1.5  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
     1.6  
     1.7 -val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
     1.8 +val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
     1.9  
    1.10  fun mk_meta_eq th =
    1.11      (case concl_of th of