--- a/src/HOL/Decision_Procs/MIR.thy Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Aug 19 11:02:14 2010 +0200
@@ -5845,9 +5845,9 @@
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);