From: Anthony F. <ac...@us...> - 2003-05-02 10:37:03
|
Update of /cvsroot/hol/hol98/src/q In directory sc8-pr-cvs1:/tmp/cvs-serv19958 Modified Files: Q.sml Log Message: Want matching on the goal and not on the assumption list (to avoid abbreviating previous abbreviations created using the same pattern), and do not abbreviate variables or constants (this isn't helpful and can be done with ABBREV_TAC). Index: Q.sml =================================================================== RCS file: /cvsroot/hol/hol98/src/q/Q.sml,v retrieving revision 1.21 retrieving revision 1.22 diff -b -C2 -d -r1.21 -r1.22 *** Q.sml 29 Apr 2003 03:57:55 -0000 1.21 --- Q.sml 2 May 2003 10:36:59 -0000 1.22 *************** *** 280,286 **** | UNABBREV_TAC _ = raise Q_ERR "UNABBREV_TAC" "unexpected quote format" - fun find' f [] = NONE - | find' f (h::t) = case f h of NONE => find' f t | x => x - fun PAT_ABBREV_TAC q (g as (asl, w)) = let val fv_set = FVL (w::asl) empty_tmset --- 280,283 ---- *************** *** 290,294 **** val l = variant (HOLset.listItems (FVL [r] fv_set)) l in ! case find' (Lib.total (find_term (can matchr))) (w::asl) of NONE => raise Q_ERR "PAT_ABBREV_TAC" "No matching term found" | SOME t => --- 287,291 ---- val l = variant (HOLset.listItems (FVL [r] fv_set)) l in ! case Lib.total (find_term (fn t => not (is_var t orelse is_const t) andalso can matchr t)) w of NONE => raise Q_ERR "PAT_ABBREV_TAC" "No matching term found" | SOME t => |