changeset 38795 | 848be46708dc |
parent 38786 | e46e7a9cb622 |
child 38864 | 4abe644fcea5 |
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 10:55:20 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 10:56:46 2010 +0200 @@ -221,8 +221,8 @@ @{const_name HOL.implies}, @{const_name All}, @{const_name Ex}, - @{const_name "op &"}, - @{const_name "op |"}] + @{const_name HOL.conj}, + @{const_name HOL.disj}] fun special_cases (c, T) = member (op =) [ @{const_name Product_Type.Unity},