# HG changeset patch
# User berghofe
# Date 1127672264 -7200
# Node ID 6de497c99e4c9aae761737310a4d1b5b054981fa
# Parent  409983bbaf00c729da8b38e67389265d38d17c8b
Fixed print mode problem in test_term.

diff -r 409983bbaf00 -r 6de497c99e4c src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Sep 25 20:17:13 2005 +0200
+++ b/src/Pure/codegen.ML	Sun Sep 25 20:17:44 2005 +0200
@@ -918,7 +918,7 @@
 
 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
 
-fun test_term thy sz i = setmp print_mode [] (fn t =>
+fun test_term thy sz i t =
   let
     val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
       "Term to be tested contains type variables";
@@ -929,7 +929,7 @@
       map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
     val (code, gr) = setmp mode ["term_of", "test"]
       (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
-    val s = "structure TestTerm =\nstruct\n\n" ^
+    val s = setmp print_mode [] (fn () => "structure TestTerm =\nstruct\n\n" ^
       space_implode "\n" (map snd code) ^
       "\nopen Generated;\n\n" ^ Pretty.string_of
         (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
@@ -952,7 +952,7 @@
                        [Pretty.str s'], Pretty.str ")"]]) frees')) @
                   [Pretty.str "]"])]],
             Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
-      "\n\nend;\n";
+      "\n\nend;\n") ();
     val _ = use_text Context.ml_output false s;
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
@@ -962,7 +962,7 @@
       else (priority ("Test data size: " ^ string_of_int k);
         case iter (fn () => !test_fn k) 1 of
           NONE => test (k+1) | SOME x => SOME x);
-  in test 0 end);
+  in test 0 end;
 
 fun test_goal ({size, iterations, default_type}, tvinsts) i st =
   let