src/Pure/meta_simplifier.ML
changeset 14643 130076a81b84
parent 14330 eb8b8241ef5b
child 14981 e73f8140af78
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Apr 22 10:49:30 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Apr 22 10:52:32 2004 +0200
     1.3 @@ -283,7 +283,7 @@
     1.4     (exists (apl (lhs, Logic.occs)) (rhs :: prems))
     1.5    orelse
     1.6     (null prems andalso
     1.7 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
     1.8 +    Pattern.matches (Sign.tsig_of sign) (lhs, rhs))
     1.9      (*the condition "null prems" is necessary because conditional rewrites
    1.10        with extra variables in the conditions may terminate although
    1.11        the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
    1.12 @@ -630,7 +630,7 @@
    1.13          val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
    1.14                            else Thm.cterm_match (elhs', eta_t');
    1.15          val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
    1.16 -        val prop' = #prop (rep_thm thm');
    1.17 +        val prop' = Thm.prop_of thm';
    1.18          val unconditional = (Logic.count_prems (prop',0) = 0);
    1.19          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
    1.20        in
    1.21 @@ -666,7 +666,7 @@
    1.22            in case opt of None => rews rrules | some => some end;
    1.23  
    1.24      fun sort_rrules rrs = let
    1.25 -      fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
    1.26 +      fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of
    1.27                                        Const("==",_) $ _ $ _ => true
    1.28                                        | _                   => false
    1.29        fun sort []        (re1,re2) = re1 @ re2
    1.30 @@ -701,7 +701,7 @@
    1.31  (* conversion to apply a congruence rule to a term *)
    1.32  
    1.33  fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
    1.34 -  let val {sign, ...} = rep_thm cong
    1.35 +  let val sign = Thm.sign_of_thm cong
    1.36        val _ = if Sign.subsig (sign, signt) then ()
    1.37                   else error("Congruence rule from different theory")
    1.38        val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;