| changeset 38549 | d0385f2764d8 |
| parent 35625 | 9c818cab0dd0 |
| child 38558 | 32ad17fe2b9c |
--- a/src/HOL/Tools/sat_funcs.ML Thu Aug 19 10:27:12 2010 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Thu Aug 19 11:02:14 2010 +0200 @@ -217,7 +217,7 @@ (* Thm.cterm -> int option *) fun index_of_literal chyp = ( case (HOLogic.dest_Trueprop o Thm.term_of) chyp of - (Const ("Not", _) $ atom) => + (Const (@{const_name "Not"}, _) $ atom) => SOME (~ (the (Termtab.lookup atom_table atom))) | atom => SOME (the (Termtab.lookup atom_table atom))