src/HOL/Tools/Meson/meson.ML
changeset 60362 befdc10ebb42
parent 60358 aebfbcab1eb8
child 60642 48dd1cefb4ae
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 10:12:46 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 11:03:02 2015 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    val trace : bool Config.T
     1.5    val max_clauses : int Config.T
     1.6    val term_pair_of: indexname * (typ * 'a) -> term * 'a
     1.7 -  val first_order_resolve : thm -> thm -> thm
     1.8 +  val first_order_resolve : Proof.context -> thm -> thm -> thm
     1.9    val size_of_subgoals: thm -> int
    1.10    val has_too_many_clauses: Proof.context -> term -> bool
    1.11    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    1.12 @@ -98,16 +98,16 @@
    1.13  fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    1.14  
    1.15  (*FIXME: currently does not "rename variables apart"*)
    1.16 -fun first_order_resolve thA thB =
    1.17 +fun first_order_resolve ctxt thA thB =
    1.18    (case
    1.19      try (fn () =>
    1.20 -      let val thy = Thm.theory_of_thm thA
    1.21 +      let val thy = Proof_Context.theory_of ctxt
    1.22            val tmA = Thm.concl_of thA
    1.23            val Const(@{const_name Pure.imp},_) $ tmB $ _ = Thm.prop_of thB
    1.24            val tenv =
    1.25              Pattern.first_order_match thy (tmB, tmA)
    1.26                                            (Vartab.empty, Vartab.empty) |> snd
    1.27 -          val ct_pairs = map (apply2 (Thm.global_cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.28 +          val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv)
    1.29        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    1.30      SOME th => th
    1.31    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    1.32 @@ -359,11 +359,10 @@
    1.33      in (th RS spec', ctxt') end
    1.34  end;
    1.35  
    1.36 -fun apply_skolem_theorem (th, rls) =
    1.37 +fun apply_skolem_theorem ctxt (th, rls) =
    1.38    let
    1.39      fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
    1.40 -      | tryall (rl :: rls) =
    1.41 -        first_order_resolve th rl handle THM _ => tryall rls
    1.42 +      | tryall (rl :: rls) = first_order_resolve ctxt th rl handle THM _ => tryall rls
    1.43    in tryall rls end
    1.44  
    1.45  (* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    1.46 @@ -383,7 +382,7 @@
    1.47                  in  ctxt_ref := ctxt'; cnf_aux (th', ths) end
    1.48            | Const (@{const_name Ex}, _) =>
    1.49                (*existential quantifier: Insert Skolem functions*)
    1.50 -              cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
    1.51 +              cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths)
    1.52            | Const (@{const_name HOL.disj}, _) =>
    1.53                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    1.54                  all combinations of converting P, Q to CNF.*)