src/FOLP/simp.ML
changeset 59498 50b60f501b05
parent 59170 de18f8b1a5a2
child 59582 0fbed69ff081
     1.1 --- a/src/FOLP/simp.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/FOLP/simp.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -75,12 +75,12 @@
     1.4    rewrite rules are not ordered.*)
     1.5  fun net_tac net =
     1.6    SUBGOAL(fn (prem,i) =>
     1.7 -          resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i);
     1.8 +          resolve0_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i);
     1.9  
    1.10  (*match subgoal i against possible theorems indexed by lhs in the net*)
    1.11  fun lhs_net_tac net =
    1.12    SUBGOAL(fn (prem,i) =>
    1.13 -          biresolve_tac (Net.unify_term net
    1.14 +          biresolve0_tac (Net.unify_term net
    1.15                         (lhs_of (Logic.strip_assums_concl prem))) i);
    1.16  
    1.17  fun nth_subgoal i thm = nth (prems_of thm) (i - 1);
    1.18 @@ -119,7 +119,7 @@
    1.19  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    1.20          Const(s,_)$_ => member (op =) norms s | _ => false;
    1.21  
    1.22 -val refl_tac = resolve_tac refl_thms;
    1.23 +val refl_tac = resolve0_tac refl_thms;
    1.24  
    1.25  fun find_res thms thm =
    1.26      let fun find [] = error "Check Simp_Data"
    1.27 @@ -138,7 +138,7 @@
    1.28          SOME(thm',_) => thm'
    1.29        | NONE => raise THM("Simplifier: could not continue", 0, [thm]);
    1.30  
    1.31 -fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm);
    1.32 +fun res1(thm,thms,i) = one_result(resolve0_tac thms i,thm);
    1.33  
    1.34  
    1.35  (**** Adding "NORM" tags ****)
    1.36 @@ -204,10 +204,10 @@
    1.37      fun norm_step_tac st = st |>
    1.38           (case head_of(rhs_of_eq 1 st) of
    1.39              Var(ixn,_) => if member (op =) hvs ixn then refl1_tac
    1.40 -                          else resolve_tac normI_thms 1 ORELSE refl1_tac
    1.41 -          | Const _ => resolve_tac normI_thms 1 ORELSE
    1.42 -                       resolve_tac congs 1 ORELSE refl1_tac
    1.43 -          | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    1.44 +                          else resolve0_tac normI_thms 1 ORELSE refl1_tac
    1.45 +          | Const _ => resolve0_tac normI_thms 1 ORELSE
    1.46 +                       resolve0_tac congs 1 ORELSE refl1_tac
    1.47 +          | Free _ => resolve0_tac congs 1 ORELSE refl1_tac
    1.48            | _ => refl1_tac)
    1.49      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    1.50      val SOME(thm'',_) = Seq.pull(add_norm_tac thm')