src/HOL/Tools/Function/function_lib.ML

       (Free v) => lambda (Free v) t
     | (Var v) => lambda (Var v) t
     | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
       (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
     | _ => raise Match
-                 
-                 
+
+
 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
     let
       val (n, body) = Term.dest_abs a
     in
       (Free (n, T), body)
     end
   | dest_all _ = raise Match
-                         
+
 
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
 fun dest_all_all (t as (Const ("all",_) $ _)) = 
     let
       val (v,b) = dest_all t
       val (vs, b') = dest_all_all b
     in
       (v :: vs, b')
     end
   | dest_all_all t = ([],t)
-                     
+
 
 (* FIXME: similar to Variable.focus *)
 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
     let
       val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]

    val thy = theory_of_cterm ct
  in
    Goal.prove_internal []
      (cterm_of thy
        (Logic.mk_equals (t,
-          if is = []
+          if null is
           then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
-          else if js = []
+          else if null js
             then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
             else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
      (K (rewrite_goals_tac ac
          THEN rtac Drule.reflexive_thm 1))
  end