src/HOL/Import/shuffler.ML
changeset 24634 38db11874724
parent 22902 ac833b4bb7ee
child 26277 461e11226111
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Sep 18 18:05:34 2007 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Sep 18 18:05:37 2007 +0200
     1.3 @@ -58,8 +58,8 @@
     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 = Library.setmp print_mode [] string_of_thm;
     1.8 -val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
     1.9 +val string_of_thm = PrintMode.setmp [] string_of_thm;
    1.10 +val string_of_cterm = PrintMode.setmp [] string_of_cterm;
    1.11  
    1.12  fun mk_meta_eq th =
    1.13      (case concl_of th of