1.1 --- a/src/HOL/Tools/meson.ML Tue Jun 13 23:41:34 2006 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Tue Jun 13 23:41:37 2006 +0200
1.3 @@ -72,7 +72,7 @@
1.4 (*raises exception if no rules apply -- unlike RL*)
1.5 fun tryres (th, rls) =
1.6 let fun tryall [] = raise THM("tryres", 0, th::rls)
1.7 - | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls)
1.8 + | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls)
1.9 in tryall rls end;
1.10
1.11 (*Permits forward proof from rules that discharge assumptions*)
1.12 @@ -84,7 +84,7 @@
1.13
1.14 (*Are any of the constants in "bs" present in the term?*)
1.15 fun has_consts bs =
1.16 - let fun has (Const(a,_)) = a mem bs
1.17 + let fun has (Const(a,_)) = member (op =) bs a
1.18 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false
1.19 (*ignore constants within @-terms*)
1.20 | has (f$u) = has f orelse has u
1.21 @@ -266,7 +266,7 @@
1.22 (*Is the string the name of a connective? It doesn't matter if this list is
1.23 incomplete, since when actually called, the only connectives likely to
1.24 remain are & | Not.*)
1.25 -fun is_conn c = c mem_string
1.26 +val is_conn = member (op =)
1.27 ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not",
1.28 "All", "Ex", "Ball", "Bex"];
1.29
1.30 @@ -336,7 +336,7 @@
1.31 | has_reps [_] = false
1.32 | has_reps [t,u] = (t aconv u)
1.33 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
1.34 - handle INSERT => true;
1.35 + handle Net.INSERT => true;
1.36
1.37 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
1.38 fun TRYING_eq_assume_tac 0 st = Seq.single st