1.1 --- a/src/HOL/Tools/meson.ML Sat Jul 15 18:17:47 2006 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Sun Jul 16 14:26:22 2006 +0200
1.3 @@ -82,13 +82,15 @@
1.4 | NONE => raise THM("forward_res", 0, [st]);
1.5
1.6
1.7 -(*Are any of the constants in "bs" present in the term?*)
1.8 -fun has_consts bs =
1.9 - let fun has (Const(a,_)) = member (op =) bs a
1.10 - | has (Const ("Hilbert_Choice.Eps",_) $ _) = false
1.11 - (*ignore constants within @-terms*)
1.12 - | has (f$u) = has f orelse has u
1.13 - | has (Abs(_,_,t)) = has t
1.14 +(*Are any of the logical connectives in "bs" present in the term?*)
1.15 +fun has_conns bs =
1.16 + let fun has (Const(a,_)) = false
1.17 + | has (Const("Trueprop",_) $ p) = has p
1.18 + | has (Const("Not",_) $ p) = has p
1.19 + | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
1.20 + | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
1.21 + | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
1.22 + | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
1.23 | has _ = false
1.24 in has end;
1.25
1.26 @@ -194,7 +196,7 @@
1.27 fun cnf skoths (th,ths) =
1.28 let fun cnf_aux (th,ths) =
1.29 if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
1.30 - else if not (has_consts ["All","Ex","op &"] (prop_of th))
1.31 + else if not (has_conns ["All","Ex","op &"] (prop_of th))
1.32 then th::ths (*no work to do, terminate*)
1.33 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
1.34 Const ("op &", _) => (*conjunction*)
1.35 @@ -410,7 +412,7 @@
1.36 (*Pull existential quantifiers to front. This accomplishes Skolemization for
1.37 clauses that arise from a subgoal.*)
1.38 fun skolemize th =
1.39 - if not (has_consts ["Ex"] (prop_of th)) then th
1.40 + if not (has_conns ["Ex"] (prop_of th)) then th
1.41 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
1.42 disj_exD, disj_exD1, disj_exD2])))
1.43 handle THM _ =>