src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
 changeset 38558 32ad17fe2b9c parent 38552 6c8806696bed child 38795 848be46708dc
1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 16:08:54 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Aug 19 16:08:59 2010 +0200
1.3 @@ -411,7 +411,7 @@
1.4  fun conjuncts t = conjuncts_aux t [];
1.6  fun is_equationlike_term (Const ("==", _) \$ _ \$ _) = true
1.7 -  | is_equationlike_term (Const (@{const_name "Trueprop"}, _) \$ (Const (@{const_name "op ="}, _) \$ _ \$ _)) = true
1.8 +  | is_equationlike_term (Const (@{const_name Trueprop}, _) \$ (Const (@{const_name "op ="}, _) \$ _ \$ _)) = true
1.9    | is_equationlike_term _ = false
1.11  val is_equationlike = is_equationlike_term o prop_of
1.12 @@ -479,7 +479,7 @@
1.14  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
1.16 -fun strip_ex (Const (@{const_name "Ex"}, _) \$ Abs (x, T, t)) =
1.17 +fun strip_ex (Const (@{const_name Ex}, _) \$ Abs (x, T, t)) =
1.18    let
1.19      val (xTs, t') = strip_ex t
1.20    in