src/HOL/Tools/Meson/meson.ML
changeset 58963 26bf09b95dda
parent 58957 c9e744ea8a38
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -30,8 +30,8 @@
     1.4    val make_clauses_unsorted: Proof.context -> thm list -> thm list
     1.5    val make_clauses: Proof.context -> thm list -> thm list
     1.6    val make_horns: thm list -> thm list
     1.7 -  val best_prolog_tac: (thm -> int) -> thm list -> tactic
     1.8 -  val depth_prolog_tac: thm list -> tactic
     1.9 +  val best_prolog_tac: Proof.context -> (thm -> int) -> thm list -> tactic
    1.10 +  val depth_prolog_tac: Proof.context -> thm list -> tactic
    1.11    val gocls: thm list -> thm list
    1.12    val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
    1.13    val MESON:
    1.14 @@ -503,8 +503,8 @@
    1.15  
    1.16  
    1.17  (* net_resolve_tac actually made it slower... *)
    1.18 -fun prolog_step_tac horns i =
    1.19 -    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
    1.20 +fun prolog_step_tac ctxt horns i =
    1.21 +    (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
    1.22      TRYALL_eq_assume_tac;
    1.23  
    1.24  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
    1.25 @@ -690,11 +690,11 @@
    1.26  (*Could simply use nprems_of, which would count remaining subgoals -- no
    1.27    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
    1.28  
    1.29 -fun best_prolog_tac sizef horns =
    1.30 -    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
    1.31 +fun best_prolog_tac ctxt sizef horns =
    1.32 +    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1);
    1.33  
    1.34 -fun depth_prolog_tac horns =
    1.35 -    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
    1.36 +fun depth_prolog_tac ctxt horns =
    1.37 +    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1);
    1.38  
    1.39  (*Return all negative clauses, as possible goal clauses*)
    1.40  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    1.41 @@ -723,7 +723,7 @@
    1.42      (fn cls =>
    1.43           THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
    1.44                           (has_fewer_prems 1, sizef)
    1.45 -                         (prolog_step_tac (make_horns cls) 1))
    1.46 +                         (prolog_step_tac ctxt (make_horns cls) 1))
    1.47      ctxt
    1.48  
    1.49  (*First, breaks the goal into independent units*)
    1.50 @@ -734,7 +734,7 @@
    1.51  
    1.52  fun depth_meson_tac ctxt =
    1.53    MESON all_tac (make_clauses ctxt)
    1.54 -    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)])
    1.55 +    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
    1.56      ctxt
    1.57  
    1.58  (** Iterative deepening version **)
    1.59 @@ -747,7 +747,7 @@
    1.60          val nrtac = net_resolve_tac horns
    1.61      in  fn i => eq_assume_tac i ORELSE
    1.62                  match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
    1.63 -                ((assume_tac i APPEND nrtac i) THEN check_tac)
    1.64 +                ((assume_tac ctxt i APPEND nrtac i) THEN check_tac)
    1.65      end;
    1.66  
    1.67  fun iter_deepen_prolog_tac ctxt horns =