1.1 --- a/src/HOL/Tools/meson.ML	Wed Jul 12 21:19:27 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jul 13 12:31:00 2006 +0200
     1.3 @@ -134,15 +134,19 @@
     1.4    
     1.5  val not_refl_disj_D = thm"meson_not_refl_disj_D";
     1.6  
     1.7 +(*Is either term a Var that does not properly occur in the other term?*)
     1.8 +fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
     1.9 +  | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
    1.10 +  | eliminable _ = false;
    1.11 +
    1.12  fun refl_clause_aux 0 th = th
    1.13    | refl_clause_aux n th =
    1.14         case HOLogic.dest_Trueprop (concl_of th) of
    1.15  	  (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => 
    1.16              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
    1.17  	| (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 
    1.18 -	    if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*)
    1.19 -		(refl_clause_aux (n-1) (th RS not_refl_disj_D)    (*delete*)
    1.20 -		 handle THM _ => refl_clause_aux (n-1) (th RS disj_comm))  (*ignore*)
    1.21 +	    if eliminable(t,u) 
    1.22 +	    then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
    1.23  	    else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
    1.24  	| (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
    1.25  	| _ => (*not a disjunction*) th;