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.5  
     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.10    
    1.11  val is_equationlike = is_equationlike_term o prop_of 
    1.12 @@ -479,7 +479,7 @@
    1.13  
    1.14  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
    1.15  
    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