src/HOL/Tools/meson.ML
changeset 32231 95b8afcbb0ed
parent 32091 30e2ffbba718
child 32262 73cd8f74cf2a
     1.1 --- a/src/HOL/Tools/meson.ML	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Jul 27 20:45:40 2009 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4                  Display.string_of_thm_without_context st ::
     1.5                  "Premises:" :: map Display.string_of_thm_without_context prems))
     1.6    in
     1.7 -    case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
     1.8 +    case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
     1.9      of SOME(th,_) => th
    1.10       | NONE => raise THM("forward_res", 0, [st])
    1.11    end;
    1.12 @@ -226,7 +226,7 @@
    1.13  fun forward_res2 nf hyps st =
    1.14    case Seq.pull
    1.15          (REPEAT
    1.16 -         (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    1.17 +         (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    1.18           st)
    1.19    of SOME(th,_) => th
    1.20     | NONE => raise THM("forward_res2", 0, [st]);
    1.21 @@ -335,8 +335,8 @@
    1.22                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    1.23                  all combinations of converting P, Q to CNF.*)
    1.24                let val tac =
    1.25 -                  (METAHYPS (resop cnf_nil) 1) THEN
    1.26 -                   (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
    1.27 +                  (OldGoals.METAHYPS (resop cnf_nil) 1) THEN
    1.28 +                   (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
    1.29                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    1.30            | _ => nodups th :: ths  (*no work to do*)
    1.31        and cnf_nil th = cnf_aux (th,[])
    1.32 @@ -584,9 +584,9 @@
    1.33    SELECT_GOAL
    1.34      (EVERY [ObjectLogic.atomize_prems_tac 1,
    1.35              rtac ccontr 1,
    1.36 -            METAHYPS (fn negs =>
    1.37 +            OldGoals.METAHYPS (fn negs =>
    1.38                        EVERY1 [skolemize_prems_tac negs,
    1.39 -                              METAHYPS (cltac o mkcl)]) 1]) i st
    1.40 +                              OldGoals.METAHYPS (cltac o mkcl)]) 1]) i st
    1.41    handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
    1.42  
    1.43  (** Best-first search versions **)
    1.44 @@ -698,7 +698,7 @@
    1.45  fun skolemize_tac i st =
    1.46    let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
    1.47    in
    1.48 -     EVERY' [METAHYPS
    1.49 +     EVERY' [OldGoals.METAHYPS
    1.50              (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
    1.51                           THEN REPEAT (etac exE 1))),
    1.52              REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st