src/FOLP/simp.ML
changeset 19805 854404b8f738
parent 17325 d9d50222808e
child 19876 11d447d5d68c
     1.1 --- a/src/FOLP/simp.ML	Wed Jun 07 01:59:17 2006 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Jun 07 02:01:27 2006 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  functor SimpFun (Simp_data: SIMP_DATA) : SIMP = 
     1.5  struct
     1.6  
     1.7 -local open Simp_data Logic in
     1.8 +local open Simp_data in
     1.9  
    1.10  (*For taking apart reductions into left, right hand sides*)
    1.11  val lhs_of = #2 o dest_red;
    1.12 @@ -76,17 +76,17 @@
    1.13    rewrite rules are not ordered.*)
    1.14  fun net_tac net =
    1.15    SUBGOAL(fn (prem,i) => 
    1.16 -          resolve_tac (Net.unify_term net (strip_assums_concl prem)) i);
    1.17 +          resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i);
    1.18  
    1.19  (*match subgoal i against possible theorems indexed by lhs in the net*)
    1.20  fun lhs_net_tac net =
    1.21    SUBGOAL(fn (prem,i) => 
    1.22            biresolve_tac (Net.unify_term net
    1.23 -                       (lhs_of (strip_assums_concl prem))) i);
    1.24 +                       (lhs_of (Logic.strip_assums_concl prem))) i);
    1.25  
    1.26  fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
    1.27  
    1.28 -fun goal_concl i thm = strip_assums_concl(nth_subgoal i thm);
    1.29 +fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm);
    1.30  
    1.31  fun lhs_of_eq i thm = lhs_of(goal_concl i thm)
    1.32  and rhs_of_eq i thm = rhs_of(goal_concl i thm);
    1.33 @@ -151,7 +151,7 @@
    1.34        | _ => ""                 (*a placeholder distinct from const names*);
    1.35  
    1.36  (*true if the term is an atomic proposition (no ==> signs) *)
    1.37 -val atomic = null o strip_assums_hyp;
    1.38 +val atomic = null o Logic.strip_assums_hyp;
    1.39  
    1.40  (*ccs contains the names of the constants possessing congruence rules*)
    1.41  fun add_hidden_vars ccs =
    1.42 @@ -381,8 +381,8 @@
    1.43  (*Select subgoal i from proof state; substitute parameters, for printing*)
    1.44  fun prepare_goal i st =
    1.45      let val subgi = nth_subgoal i st
    1.46 -        val params = rev(strip_params subgi)
    1.47 -    in variants_abs (params, strip_assums_concl subgi) end;
    1.48 +        val params = rev (Logic.strip_params subgi)
    1.49 +    in variants_abs (params, Logic.strip_assums_concl subgi) end;
    1.50  
    1.51  (*print lhs of conclusion of subgoal i*)
    1.52  fun pr_goal_lhs i st =
    1.53 @@ -426,8 +426,8 @@
    1.54              SOME(thm',_) =>
    1.55                      let val ps = prems_of thm and ps' = prems_of thm';
    1.56                          val n = length(ps')-length(ps);
    1.57 -                        val a = length(strip_assums_hyp(List.nth(ps,i-1)))
    1.58 -                        val l = map (fn p => length(strip_assums_hyp(p)))
    1.59 +                        val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1)))
    1.60 +                        val l = map (fn p => length(Logic.strip_assums_hyp(p)))
    1.61                                      (Library.take(n,Library.drop(i-1,ps')));
    1.62                      in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
    1.63            | NONE => (REW::ss,thm,anet,ats,cs);