src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 38864 4abe644fcea5
parent 38829 c18e8f90f4dc
child 38907 245fca4ce86f
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4     handled specially via "fequal". *)
     1.5  val boring_consts =
     1.6    [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
     1.7 -   @{const_name "op ="}]
     1.8 +   @{const_name HOL.eq}]
     1.9  
    1.10  (* Add a pconstant to the table, but a [] entry means a standard
    1.11     connective, which we ignore.*)
    1.12 @@ -177,7 +177,7 @@
    1.13        | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
    1.14        | @{const HOL.implies} $ t1 $ t2 =>
    1.15          do_formula (flip pos) t1 #> do_formula pos t2
    1.16 -      | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
    1.17 +      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
    1.18          fold (do_term_or_formula T) [t1, t2]
    1.19        | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
    1.20          $ t1 $ t2 $ t3 =>
    1.21 @@ -557,7 +557,7 @@
    1.22        | (_, @{const Not} $ t1) => do_formula (not pos) t1
    1.23        | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    1.24        | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    1.25 -      | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
    1.26 +      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
    1.27        | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
    1.28        | _ => false
    1.29    in do_formula true end