src/q/Q.sml

436 fun wholeterm_rename_helper {pats,fvs_set,ERR,kont} tm g = let
453   test_parses pats
466     {pats=pat_parses, ERR = ERR "MATCH_RENAME_TAC", kont = k,
475   val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) ctxt q
479       {pats=pats, ERR = ERR "MATCH_ASSUM_RENAME_TAC", kont = k,
489 fun subterm_helper make_tac k {ERR,pats,fvs_set} t g = let
513   find_pats pats
519   val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) fvs q
530   {ERR = ERR, pats = seq.map mapthis pats, fvs_set = fvs_set}