# HG changeset patch
# User berghofe
# Date 1089383037 -7200
# Node ID a4d0ed993050e4df0129c9957bc485fea3a1b590
# Parent  f6a22afe0134c98fde7b0b4ed42e628cfb778ce2
- Removed obsolete clause in function check_str
- test_term now temporarily sets print_mode to [] as well

diff -r f6a22afe0134 -r a4d0ed993050 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Jul 09 11:13:36 2004 +0200
+++ b/src/Pure/codegen.ML	Fri Jul 09 16:23:57 2004 +0200
@@ -286,7 +286,6 @@
     fun check_str [] = []
       | check_str xs = (case take_prefix is_ascii_letdig xs of
           ([], " " :: zs) => check_str zs
-        | ([], "_" :: zs) => check_str zs
         | ([], z :: zs) =>
           if size z = 1 then string_of_int (ord z) :: check_str zs
           else (case dest_sym z of
@@ -568,7 +567,7 @@
 
 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => None);
 
-fun test_term thy sz i t =
+fun test_term thy sz i = setmp print_mode [] (fn t =>
   let
     val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
       "Term to be tested contains type variables";
@@ -611,7 +610,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