src/HOL/Tools/meson.ML
changeset 38864 4abe644fcea5
parent 38806 0aafc7e81056
child 39037 5146d640aa4a
     1.1 --- a/src/HOL/Tools/meson.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/meson.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4  fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
     1.5  
     1.6  (*Literals like X=X are tautologous*)
     1.7 -fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
     1.8 +fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
     1.9    | taut_poslit (Const(@{const_name True},_)) = true
    1.10    | taut_poslit _ = false;
    1.11  
    1.12 @@ -213,7 +213,7 @@
    1.13         case HOLogic.dest_Trueprop (concl_of th) of
    1.14            (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
    1.15              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
    1.16 -        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
    1.17 +        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
    1.18              if eliminable(t,u)
    1.19              then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
    1.20              else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
    1.21 @@ -222,7 +222,7 @@
    1.22  
    1.23  fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
    1.24        notequal_lits_count P + notequal_lits_count Q
    1.25 -  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
    1.26 +  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
    1.27    | notequal_lits_count _ = 0;
    1.28  
    1.29  (*Simplify a clause by applying reflexivity to its negated equality literals*)
    1.30 @@ -280,7 +280,7 @@
    1.31      | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
    1.32          if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
    1.33               else sum (signed_nclauses (not b) t) (signed_nclauses b u)
    1.34 -    | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
    1.35 +    | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
    1.36          if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
    1.37              if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
    1.38                            (prod (signed_nclauses (not b) u) (signed_nclauses b t))