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