src/HOL/Tools/cnf_funcs.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39035 094848cf7ef3
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4    | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _)                                    = false
     1.5    | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _)                                    = false
     1.6    | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
     1.7 -  | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
     1.8 +  | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
     1.9    | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
    1.10    | is_atom _                                                              = true;
    1.11  
    1.12 @@ -205,7 +205,7 @@
    1.13  	in
    1.14  		make_nnf_imp OF [thm1, thm2]
    1.15  	end
    1.16 -  | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
    1.17 +  | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
    1.18  	let
    1.19  		val thm1 = make_nnf_thm thy x
    1.20  		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
    1.21 @@ -239,7 +239,7 @@
    1.22  	in
    1.23  		make_nnf_not_imp OF [thm1, thm2]
    1.24  	end
    1.25 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
    1.26 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
    1.27  	let
    1.28  		val thm1 = make_nnf_thm thy x
    1.29  		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)