--- a/src/HOL/Tools/prop_logic.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML Thu Aug 19 16:08:59 2010 +0200
@@ -391,11 +391,11 @@
next_idx_is_valid := true;
Unsynchronized.inc next_idx
)
- fun aux (Const (@{const_name "True"}, _)) table =
+ fun aux (Const (@{const_name True}, _)) table =
(True, table)
- | aux (Const (@{const_name "False"}, _)) table =
+ | aux (Const (@{const_name False}, _)) table =
(False, table)
- | aux (Const (@{const_name "Not"}, _) $ x) table =
+ | aux (Const (@{const_name Not}, _) $ x) table =
apfst Not (aux x table)
| aux (Const (@{const_name "op |"}, _) $ x $ y) table =
let