--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 19 16:08:59 2010 +0200
@@ -111,7 +111,7 @@
fun mk_meta_equation th =
case prop_of th of
- Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
| _ => th
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -215,12 +215,12 @@
val logic_operator_names =
[@{const_name "=="},
@{const_name "==>"},
- @{const_name "Trueprop"},
- @{const_name "Not"},
+ @{const_name Trueprop},
+ @{const_name Not},
@{const_name "op ="},
@{const_name "op -->"},
- @{const_name "All"},
- @{const_name "Ex"},
+ @{const_name All},
+ @{const_name Ex},
@{const_name "op &"},
@{const_name "op |"}]