changeset 37391 | 476270a6c2dc |
parent 29064 | 70a61d58460e |
child 38554 | f8999e19dd49 |
--- a/src/HOL/Tools/TFL/dcterm.ML Thu Jun 10 12:24:02 2010 +0200 +++ b/src/HOL/Tools/TFL/dcterm.ML Thu Jun 10 12:24:03 2010 +0200 @@ -129,7 +129,7 @@ val dest_neg = dest_monop "not" -val dest_pair = dest_binop "Pair"; +val dest_pair = dest_binop @{const_name Pair}; val dest_eq = dest_binop "op =" val dest_imp = dest_binop "op -->" val dest_conj = dest_binop "op &"