# HG changeset patch
# User wenzelm
# Date 1198004070 -3600
# Node ID c2058af6d9bc50f5a486b6effdecde737f3f3e6c
# Parent  7025a263aa490cd282c0819e4eee14fb9580d1ba
PrintMode.setmp (avoid direct access to print_mode ref);

diff -r 7025a263aa49 -r c2058af6d9bc src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Dec 18 19:15:31 2007 +0100
+++ b/src/HOL/Statespace/state_space.ML	Tue Dec 18 19:54:30 2007 +0100
@@ -465,7 +465,7 @@
 
    fun string_of_typ T = 
       setmp show_sorts true 
-       (setmp print_mode [] (Syntax.string_of_typ (ProofContext.init thy))) T;
+       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
    val fixestate = (case state_type of
          NONE => []
        | SOME s =>