tuned;
authorwenzelm
Mon May 20 14:04:21 2013 +0200 (2013-05-20)
changeset 52082559e1398b70e
parent 52081 29566b6810f7
child 52083 f852d08376f9
tuned;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Mon May 20 13:54:24 2013 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon May 20 14:04:21 2013 +0200
     1.3 @@ -578,7 +578,7 @@
     1.4  
     1.5  (*create the rewrite rule and possibly also the eq_True variant,
     1.6    in case there are extra vars on the rhs*)
     1.7 -fun rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm2) =
     1.8 +fun rrule_eq_True ctxt thm name lhs elhs rhs thm2 =
     1.9    let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
    1.10      if rewrite_rule_extra_vars [] lhs rhs then
    1.11        mk_eq_True ctxt (thm2, name) @ [rrule]
    1.12 @@ -592,7 +592,7 @@
    1.13        (*weak test for loops*)
    1.14        if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
    1.15        then mk_eq_True ctxt (thm, name)
    1.16 -      else rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm)
    1.17 +      else rrule_eq_True ctxt thm name lhs elhs rhs thm
    1.18    end;
    1.19  
    1.20  fun orient_rrule ctxt (thm, name) =
    1.21 @@ -609,8 +609,8 @@
    1.22            NONE => []
    1.23          | SOME thm' =>
    1.24              let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
    1.25 -            in rrule_eq_True (thm', name, lhs', elhs', rhs', ctxt, thm) end)
    1.26 -    else rrule_eq_True (thm, name, lhs, elhs, rhs, ctxt, thm)
    1.27 +            in rrule_eq_True ctxt thm' name lhs' elhs' rhs' thm end)
    1.28 +    else rrule_eq_True ctxt thm name lhs elhs rhs thm
    1.29    end;
    1.30  
    1.31  fun extract_rews (ctxt, thms) =