# HG changeset patch # User wenzelm # Date 1481041434 -3600 # Node ID 8b187a7a9776dbad9fd532232305e14259d077dc # Parent a955511171a847cc051647d7c7d2184ba952e59f avoid spurious messages -- potential cause of problems for "meson"; diff -r a955511171a8 -r 8b187a7a9776 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Tue Dec 06 17:21:34 2016 +0100 +++ b/src/Tools/misc_legacy.ML Tue Dec 06 17:23:54 2016 +0100 @@ -201,26 +201,10 @@ (false, relift st, Thm.nprems_of st) gno state in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end; -fun print_vars_terms ctxt n thm = - let - fun typed s ty = " " ^ s ^ " has type: " ^ Syntax.string_of_typ ctxt ty; - fun find_vars (Const (c, ty)) = - if null (Term.add_tvarsT ty []) then I - else insert (op =) (typed c ty) - | find_vars (Var (xi, ty)) = - insert (op =) (typed (Term.string_of_vname xi) ty) - | find_vars (Free _) = I - | find_vars (Bound _) = I - | find_vars (Abs (_, _, t)) = find_vars t - | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2; - val prem = Logic.nth_prem (n, Thm.prop_of thm) - val tms = find_vars prem [] - in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end; - in fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm - handle THM ("assume: variables", _, _) => (print_vars_terms ctxt n thm; Seq.empty) + handle THM ("assume: variables", _, _) => Seq.empty end;