src/HOL/Tools/res_axioms.ML
changeset 32231 95b8afcbb0ed
parent 32091 30e2ffbba718
child 32257 bad5a99c16d8
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Jul 27 20:45:40 2009 +0200
     1.3 @@ -503,8 +503,8 @@
     1.4  
     1.5  fun neg_conjecture_clauses st0 n =
     1.6    let val st = Seq.hd (neg_skolemize_tac n st0)
     1.7 -      val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
     1.8 -  in (neg_clausify (the (metahyps_thms n st)), params) end
     1.9 +      val (params,_,_) = OldGoals.strip_context (Logic.nth_prem (n, Thm.prop_of st))
    1.10 +  in (neg_clausify (the (OldGoals.metahyps_thms n st)), params) end
    1.11    handle Option => error "unable to Skolemize subgoal";
    1.12  
    1.13  (*Conversion of a subgoal to conjecture clauses. Each clause has
    1.14 @@ -515,7 +515,7 @@
    1.15      (fn (prop,_) =>
    1.16       let val ts = Logic.strip_assums_hyp prop
    1.17       in EVERY1
    1.18 -         [METAHYPS
    1.19 +         [OldGoals.METAHYPS
    1.20              (fn hyps =>
    1.21                (Method.insert_tac
    1.22                  (map forall_intr_vars (neg_clausify hyps)) 1)),