src/HOL/Tools/Metis/metis_tactic.ML
changeset 60358 aebfbcab1eb8
parent 59632 5980e75a204e
child 60362 befdc10ebb42
     1.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -32,8 +32,9 @@
     1.4  val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
     1.5  
     1.6  (* Designed to work also with monomorphic instances of polymorphic theorems. *)
     1.7 -fun have_common_thm ths1 ths2 =
     1.8 -  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) (map Meson.make_meta_clause ths2)
     1.9 +fun have_common_thm ctxt ths1 ths2 =
    1.10 +  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
    1.11 +    (map (Meson.make_meta_clause ctxt) ths2)
    1.12  
    1.13  (*Determining which axiom clauses are actually used*)
    1.14  fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
    1.15 @@ -54,14 +55,14 @@
    1.16      (if can HOLogic.dest_not t1 then t2 else t1)
    1.17      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
    1.18    | _ => raise Fail "expected reflexive or trivial clause")
    1.19 -  |> Meson.make_meta_clause
    1.20 +  |> Meson.make_meta_clause ctxt
    1.21  
    1.22  fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
    1.23    let
    1.24      val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
    1.25      val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
    1.26      val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    1.27 -  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
    1.28 +  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause ctxt end
    1.29  
    1.30  fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
    1.31    | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
    1.32 @@ -201,7 +202,7 @@
    1.33           val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
    1.34           val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
    1.35           val (used_th_cls_pairs, unused_th_cls_pairs) =
    1.36 -           List.partition (have_common_thm used o snd o snd) th_cls_pairs
    1.37 +           List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
    1.38           val unused_ths = maps (snd o snd) unused_th_cls_pairs
    1.39           val unused_names = map fst unused_th_cls_pairs
    1.40         in
    1.41 @@ -210,7 +211,7 @@
    1.42             verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names)
    1.43           else
    1.44             ();
    1.45 -         if not (null cls) andalso not (have_common_thm used cls) then
    1.46 +         if not (null cls) andalso not (have_common_thm ctxt used cls) then
    1.47             verbose_warning ctxt "The assumptions are inconsistent"
    1.48           else
    1.49             ();