src/HOL/Tools/Meson/meson.ML
changeset 58957 c9e744ea8a38
parent 58839 ccda99401bc8
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -40,8 +40,8 @@
     1.4    val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
     1.5    val safe_best_meson_tac: Proof.context -> int -> tactic
     1.6    val depth_meson_tac: Proof.context -> int -> tactic
     1.7 -  val prolog_step_tac': thm list -> int -> tactic
     1.8 -  val iter_deepen_prolog_tac: thm list -> tactic
     1.9 +  val prolog_step_tac': Proof.context -> thm list -> int -> tactic
    1.10 +  val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic
    1.11    val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
    1.12    val make_meta_clause: thm -> thm
    1.13    val make_meta_clauses: thm list -> thm list
    1.14 @@ -741,17 +741,17 @@
    1.15  
    1.16  (*This version does only one inference per call;
    1.17    having only one eq_assume_tac speeds it up!*)
    1.18 -fun prolog_step_tac' horns =
    1.19 +fun prolog_step_tac' ctxt horns =
    1.20      let val (horn0s, _) = (*0 subgoals vs 1 or more*)
    1.21              take_prefix Thm.no_prems horns
    1.22          val nrtac = net_resolve_tac horns
    1.23      in  fn i => eq_assume_tac i ORELSE
    1.24 -                match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
    1.25 +                match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
    1.26                  ((assume_tac i APPEND nrtac i) THEN check_tac)
    1.27      end;
    1.28  
    1.29 -fun iter_deepen_prolog_tac horns =
    1.30 -    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
    1.31 +fun iter_deepen_prolog_tac ctxt horns =
    1.32 +    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns);
    1.33  
    1.34  fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
    1.35    (fn cls =>
    1.36 @@ -766,7 +766,7 @@
    1.37                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
    1.38          in
    1.39            THEN_ITER_DEEPEN iter_deepen_limit
    1.40 -            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
    1.41 +            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
    1.42          end));
    1.43  
    1.44  fun meson_tac ctxt ths =