avoid spurious messages -- potential cause of problems for "meson";
authorwenzelm
Tue Dec 06 17:23:54 2016 +0100 (13 months ago)
changeset 645488b187a7a9776
parent 64547 a955511171a8
child 64549 964ac7439a52
avoid spurious messages -- potential cause of problems for "meson";
src/Tools/misc_legacy.ML
     1.1 --- a/src/Tools/misc_legacy.ML	Tue Dec 06 17:21:34 2016 +0100
     1.2 +++ b/src/Tools/misc_legacy.ML	Tue Dec 06 17:23:54 2016 +0100
     1.3 @@ -201,26 +201,10 @@
     1.4            (false, relift st, Thm.nprems_of st) gno state
     1.5    in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end;
     1.6  
     1.7 -fun print_vars_terms ctxt n thm =
     1.8 -  let
     1.9 -    fun typed s ty = "  " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty;
    1.10 -    fun find_vars (Const (c, ty)) =
    1.11 -          if null (Term.add_tvarsT ty []) then I
    1.12 -          else insert (op =) (typed c ty)
    1.13 -      | find_vars (Var (xi, ty)) =
    1.14 -          insert (op =) (typed (Term.string_of_vname xi) ty)
    1.15 -      | find_vars (Free _) = I
    1.16 -      | find_vars (Bound _) = I
    1.17 -      | find_vars (Abs (_, _, t)) = find_vars t
    1.18 -      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
    1.19 -    val prem = Logic.nth_prem (n, Thm.prop_of thm)
    1.20 -    val tms = find_vars prem []
    1.21 -  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
    1.22 -
    1.23  in
    1.24  
    1.25  fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm
    1.26 -  handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty)
    1.27 +  handle THM ("assume: variables", _, _) => Seq.empty
    1.28  
    1.29  end;
    1.30