src/HOL/Tools/meson.ML
changeset 37781 2fbbf0a48cef
parent 37539 c80e77e8d036
child 37926 e6ff246c0cdb
     1.1 --- a/src/HOL/Tools/meson.ML	Mon Jul 12 21:12:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Jul 12 21:38:37 2010 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4                  Display.string_of_thm ctxt st ::
     1.5                  "Premises:" :: map (Display.string_of_thm ctxt) prems))
     1.6    in
     1.7 -    case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
     1.8 +    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
     1.9      of SOME(th,_) => th
    1.10       | NONE => raise THM("forward_res", 0, [st])
    1.11    end;
    1.12 @@ -234,7 +234,7 @@
    1.13  fun forward_res2 ctxt nf hyps st =
    1.14    case Seq.pull
    1.15          (REPEAT
    1.16 -         (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    1.17 +         (Misc_Legacy.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 @@ -345,8 +345,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 -                  OldGoals.METAHYPS (resop cnf_nil) 1 THEN
    1.26 -                   (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
    1.27 +                  Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
    1.28 +                   (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
    1.29                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    1.30            | _ => nodups ctxt th :: ths  (*no work to do*)
    1.31        and cnf_nil th = cnf_aux (th,[])
    1.32 @@ -706,7 +706,7 @@
    1.33    let val ts = Logic.strip_assums_hyp goal
    1.34    in
    1.35      EVERY'
    1.36 -     [OldGoals.METAHYPS (fn hyps =>
    1.37 +     [Misc_Legacy.METAHYPS (fn hyps =>
    1.38          (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
    1.39            THEN REPEAT (etac exE 1))),
    1.40        REPEAT_DETERM_N (length ts) o (etac thin_rl)] i