src/Pure/thm.ML
changeset 19861 620d90091788
parent 19525 0cd0bf32ac58
child 19881 47937afefdc9
     1.1 --- a/src/Pure/thm.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/Pure/thm.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -951,7 +951,7 @@
     1.4    Resulting sequence may contain multiple elements if the tpairs are
     1.5      not all flex-flex. *)
     1.6  fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
     1.7 -  Unify.smash_unifiers (Theory.deref thy_ref, Envir.empty maxidx, tpairs)
     1.8 +  Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx)
     1.9    |> Seq.map (fn env =>
    1.10        if Envir.is_empty env then th
    1.11        else
    1.12 @@ -1426,7 +1426,7 @@
    1.13               if Envir.is_empty env then (tpairs, (Bs @ As, C))
    1.14               else
    1.15               let val ntps = map (pairself normt) tpairs
    1.16 -             in if Envir.above (smax, env) then
    1.17 +             in if Envir.above env smax then
    1.18                    (*no assignments in state; normalize the rule only*)
    1.19                    if lifted
    1.20                    then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
    1.21 @@ -1439,7 +1439,7 @@
    1.22               Thm{thy_ref = thy_ref,
    1.23                   der = Pt.infer_derivs
    1.24                     ((if Envir.is_empty env then I
    1.25 -                     else if Envir.above (smax, env) then
    1.26 +                     else if Envir.above env smax then
    1.27                         (fn f => fn der => f (Pt.norm_proof' env der))
    1.28                       else
    1.29                         curry op oo (Pt.norm_proof' env))