1.1 --- a/src/Pure/old_goals.ML	Fri Jun 04 15:43:02 2010 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Fri Jun 04 16:53:08 2010 +0200
     1.3 @@ -189,28 +189,28 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun print_vars_terms thy (n,thm) =
     1.8 +fun print_vars_terms n thm =
     1.9    let
    1.10 -    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
    1.11 -    fun find_vars thy (Const (c, ty)) =
    1.12 +    val thy = theory_of_thm thm
    1.13 +    fun typed s ty =
    1.14 +      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
    1.15 +    fun find_vars (Const (c, ty)) =
    1.16            if null (Term.add_tvarsT ty []) then I
    1.17 -          else insert (op =) (c ^ typed ty)
    1.18 -      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
    1.19 -      | find_vars _ (Free _) = I
    1.20 -      | find_vars _ (Bound _) = I
    1.21 -      | find_vars thy (Abs (_, _, t)) = find_vars thy t
    1.22 -      | find_vars thy (t1 $ t2) =
    1.23 -          find_vars thy t1 #> find_vars thy t1;
    1.24 +          else insert (op =) (typed c ty)
    1.25 +      | find_vars (Var (xi, ty)) =
    1.26 +          insert (op =) (typed (Term.string_of_vname xi) ty)
    1.27 +      | find_vars (Free _) = I
    1.28 +      | find_vars (Bound _) = I
    1.29 +      | find_vars (Abs (_, _, t)) = find_vars t
    1.30 +      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
    1.31      val prem = Logic.nth_prem (n, Thm.prop_of thm)
    1.32 -    val tms = find_vars thy prem []
    1.33 -  in
    1.34 -    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
    1.35 -  end;
    1.36 +    val tms = find_vars prem []
    1.37 +  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
    1.38  
    1.39  in
    1.40  
    1.41  fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
    1.42 -  handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
    1.43 +  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
    1.44  
    1.45  end;
    1.46