# HG changeset patch
# User wenzelm
# Date 1600953405 -7200
# Node ID c0d04c740b8a30ef5423563793be89f05d3b5083
# Parent  415220b59d37514a3565b903d9b1580bb95979cc
tuned signature;

diff -r 415220b59d37 -r c0d04c740b8a src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 00:29:51 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 15:16:45 2020 +0200
@@ -15,7 +15,6 @@
   val start_markerN: string
   val end_markerN: string
   val test_terms: Proof.context -> term list -> string -> unit
-  val test_targets: Proof.context -> term list -> string list -> unit
   val test_code_cmd: string list -> string list -> Proof.context -> unit
   val eval_term: string -> Proof.context -> term -> term
   val check_settings: string -> string -> string -> unit
@@ -232,10 +231,6 @@
     | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
   end
 
-fun test_targets ctxt = List.app o test_terms ctxt
-
-fun pretty_free ctxt = Syntax.pretty_term ctxt o Free
-
 fun test_code_cmd raw_ts targets ctxt =
   let
     val ts = Syntax.read_terms ctxt raw_ts
@@ -244,8 +239,8 @@
       if null frees then ()
       else error (Pretty.string_of
         (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
-          Pretty.commas (map (pretty_free ctxt) frees))))
-  in test_targets ctxt ts targets end
+          Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
+  in List.app (test_terms ctxt ts) targets end
 
 fun eval_term target ctxt t =
   let
@@ -255,7 +250,7 @@
       else
         error (Pretty.string_of
           (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
-            Pretty.commas (map (pretty_free ctxt) frees))))
+            Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
 
     val T = fastype_of t
     val _ =