# HG changeset patch
# User wenzelm
# Date 1147777289 -7200
# Node ID 91c0ae7e542b0784e185a6456de4a64e885912e8
# Parent  bbda28f2d379c809ef15eececfcd4eba64489871
avoid low-level Term.str_of_term;

diff -r bbda28f2d379 -r 91c0ae7e542b src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Tue May 16 13:01:28 2006 +0200
+++ b/src/Pure/tctical.ML	Tue May 16 13:01:29 2006 +0200
@@ -486,12 +486,12 @@
 
 fun print_vars_terms thy (n,thm) =
   let
+    fun typed ty = " has type: " ^ Sign.string_of_typ thy ty;
     fun find_vars thy (Const (c, ty)) =
         (case Term.typ_tvars ty
          of [] => I
-          | _ => insert (op =) (c ^ " has type: " ^ (Sign.string_of_typ thy ty)))
-      | find_vars thy (t as Var _) =
-          insert (op =) ("Var " ^ (Term.str_of_term t))
+          | _ => insert (op =) (c ^ typed ty))
+      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
       | find_vars _ (Free _) = I
       | find_vars _ (Bound _) = I
       | find_vars thy (Abs (_, _, t)) = find_vars thy t