--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 19 11:02:14 2010 +0200
@@ -86,11 +86,11 @@
map instantiate rew_ths
end
-fun is_compound ((Const ("Not", _)) $ t) =
+fun is_compound ((Const (@{const_name "Not"}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
- | is_compound ((Const ("Ex", _)) $ _) = true
+ | is_compound ((Const (@{const_name "Ex"}, _)) $ _) = true
| is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
- | is_compound ((Const ("op &", _)) $ _ $ _) =
+ | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false