# HG changeset patch
# User haftmann
# Date 1257930390 -3600
# Node ID 168b928d502403569fc22dc26ae61afa0972d203
# Parent  5c0024338ceff4063eafd58621ec48dc9b14cc2e
tuned

diff -r 5c0024338cef -r 168b928d5024 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Nov 11 10:06:30 2009 +0100
@@ -30,8 +30,8 @@
     | (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
@@ -39,7 +39,7 @@
       (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",_) $ _)) = 
@@ -50,7 +50,7 @@
       (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))) =
@@ -161,9 +161,9 @@
    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