avoid low-level Term.str_of_term;
authorwenzelm
Tue May 16 13:01:29 2006 +0200 (2006-05-16)
changeset 1964691c0ae7e542b
parent 19645 bbda28f2d379
child 19647 043921b0e587
avoid low-level Term.str_of_term;
src/Pure/tctical.ML
     1.1 --- a/src/Pure/tctical.ML	Tue May 16 13:01:28 2006 +0200
     1.2 +++ b/src/Pure/tctical.ML	Tue May 16 13:01:29 2006 +0200
     1.3 @@ -486,12 +486,12 @@
     1.4  
     1.5  fun print_vars_terms thy (n,thm) =
     1.6    let
     1.7 +    fun typed ty = " has type: " ^ Sign.string_of_typ thy ty;
     1.8      fun find_vars thy (Const (c, ty)) =
     1.9          (case Term.typ_tvars ty
    1.10           of [] => I
    1.11 -          | _ => insert (op =) (c ^ " has type: " ^ (Sign.string_of_typ thy ty)))
    1.12 -      | find_vars thy (t as Var _) =
    1.13 -          insert (op =) ("Var " ^ (Term.str_of_term t))
    1.14 +          | _ => insert (op =) (c ^ typed ty))
    1.15 +      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
    1.16        | find_vars _ (Free _) = I
    1.17        | find_vars _ (Bound _) = I
    1.18        | find_vars thy (Abs (_, _, t)) = find_vars thy t