# HG changeset patch
# User paulson
# Date 1152786660 -7200
# Node ID 7923aacc10c6bf6d94204522bd3ee23c9ebea8f6
# Parent  0c1ec587a5a8aabe4cc91ded16f44b1dd93b25c6
fix to refl_clause_aux: added occurs check

diff -r 0c1ec587a5a8 -r 7923aacc10c6 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Jul 12 21:19:27 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Jul 13 12:31:00 2006 +0200
@@ -134,15 +134,19 @@
   
 val not_refl_disj_D = thm"meson_not_refl_disj_D";
 
+(*Is either term a Var that does not properly occur in the other term?*)
+fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
+  | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
+  | eliminable _ = false;
+
 fun refl_clause_aux 0 th = th
   | refl_clause_aux n th =
        case HOLogic.dest_Trueprop (concl_of th) of
 	  (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => 
             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
 	| (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 
-	    if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*)
-		(refl_clause_aux (n-1) (th RS not_refl_disj_D)    (*delete*)
-		 handle THM _ => refl_clause_aux (n-1) (th RS disj_comm))  (*ignore*)
+	    if eliminable(t,u) 
+	    then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
 	    else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
 	| (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
 	| _ => (*not a disjunction*) th;