--- a/src/HOL/Tools/prop_logic.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML Thu Aug 19 11:02:14 2010 +0200
@@ -391,20 +391,20 @@
next_idx_is_valid := true;
Unsynchronized.inc next_idx
)
- fun aux (Const ("True", _)) table =
+ fun aux (Const (@{const_name "True"}, _)) table =
(True, table)
- | aux (Const ("False", _)) table =
+ | aux (Const (@{const_name "False"}, _)) table =
(False, table)
- | aux (Const ("Not", _) $ x) table =
+ | aux (Const (@{const_name "Not"}, _) $ x) table =
apfst Not (aux x table)
- | aux (Const ("op |", _) $ x $ y) table =
+ | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
in
(Or (fm1, fm2), table2)
end
- | aux (Const ("op &", _) $ x $ y) table =
+ | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1