src/Pure/thm.ML

 (*Smash unifies the list of term pairs leaving no flex-flex pairs.
   Instantiates the theorem and deletes trivial tpairs.
   Resulting sequence may contain multiple elements if the tpairs are
     not all flex-flex. *)
 fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
-  Unify.smash_unifiers (Theory.deref thy_ref, Envir.empty maxidx, tpairs)
+  Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx)
   |> Seq.map (fn env =>
       if Envir.is_empty env then th
       else
         let
           val tpairs' = tpairs |> map (pairself (Envir.norm_term env))

            (*perform minimal copying here by examining env*)
            val (ntpairs, normp) =
              if Envir.is_empty env then (tpairs, (Bs @ As, C))
              else
              let val ntps = map (pairself normt) tpairs
-             in if Envir.above (smax, env) then
+             in if Envir.above env smax then
                   (*no assignments in state; normalize the rule only*)
                   if lifted
                   then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
                   else (ntps, (Bs @ map normt As, C))
                 else if match then raise COMPOSE

              end
            val th =
              Thm{thy_ref = thy_ref,
                  der = Pt.infer_derivs
                    ((if Envir.is_empty env then I
-                     else if Envir.above (smax, env) then
+                     else if Envir.above env smax then
                        (fn f => fn der => f (Pt.norm_proof' env der))
                      else
                        curry op oo (Pt.norm_proof' env))
                     (Pt.bicompose_proof flatten Bs oldAs As A n)) rder' sder,
                  maxidx = maxidx,