src/HOL/Tools/Meson/meson.ML
changeset 59164 ff40c53d1af9
parent 59058 a78612c67ec0
child 59165 115965966e15
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sat Dec 20 19:12:41 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sat Dec 20 22:23:37 2014 +0100
     1.3 @@ -502,7 +502,7 @@
     1.4    then  Seq.empty  else  Seq.single st;
     1.5  
     1.6  
     1.7 -(* net_resolve_tac actually made it slower... *)
     1.8 +(* resolve_from_net_tac actually made it slower... *)
     1.9  fun prolog_step_tac ctxt horns i =
    1.10      (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
    1.11      TRYALL_eq_assume_tac;
    1.12 @@ -744,7 +744,7 @@
    1.13  fun prolog_step_tac' ctxt horns =
    1.14      let val (horn0s, _) = (*0 subgoals vs 1 or more*)
    1.15              take_prefix Thm.no_prems horns
    1.16 -        val nrtac = net_resolve_tac horns
    1.17 +        val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns)
    1.18      in  fn i => eq_assume_tac i ORELSE
    1.19                  match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
    1.20                  ((assume_tac ctxt i APPEND nrtac i) THEN check_tac)