1structure term_tactic :> term_tactic =
2struct
3
4open HolKernel Feedback Tactical
5type tactic = Tactic.tactic
6type term_tactic = Term.term -> tactic
7
8fun goal_term ttac (g as (_,w)) = ttac w g
9fun subtm_assum_term t ttac (g as (asl,w)) =
10    case List.find (free_in t) asl of
11        NONE => raise mk_HOL_ERR "term_tactic" "subtm_assum_term"
12                      ("No assumption contains " ^
13                       Parse.term_to_string t ^ " free")
14      | SOME asm => ttac asm g
15
16fun first_assum_term ttac (g as (asl,_)) = MAP_FIRST ttac asl g
17fun last_assum_term ttac (g as (asl,_)) = MAP_FIRST ttac (List.rev asl) g
18fun first_fv_term ttac (g as (asl,w)) =
19    MAP_FIRST ttac (free_varsl (w::asl)) g
20fun fv_term ttac (g as (asl,w)) =
21    let
22      fun recurse l =
23          case l of
24              [] => raise mk_HOL_ERR "term_tactic" "fv_term"
25                          "No free variables in goal"
26            | t::ts => case free_vars t of
27                           [] => recurse ts
28                         | v::_ => ttac v g
29    in
30      recurse (w::asl)
31    end
32
33end (* struct *)
34