src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 53887 ee91bd2a506a
parent 52230 1105b3b5aa77
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 25 16:29:35 2013 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 25 16:43:46 2013 +0200
     1.3 @@ -43,7 +43,6 @@
     1.4    val dest_indprem : indprem -> term
     1.5    val map_indprem : (term -> term) -> indprem -> indprem
     1.6    (* general syntactic functions *)
     1.7 -  val conjuncts : term -> term list
     1.8    val is_equationlike : thm -> bool
     1.9    val is_pred_equation : thm -> bool
    1.10    val is_intro : string -> thm -> bool
    1.11 @@ -456,12 +455,6 @@
    1.12  
    1.13  (* general syntactic functions *)
    1.14  
    1.15 -(*Like dest_conj, but flattens conjunctions however nested*)
    1.16 -fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    1.17 -  | conjuncts_aux t conjs = t::conjs;
    1.18 -
    1.19 -fun conjuncts t = conjuncts_aux t [];
    1.20 -
    1.21  fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    1.22    | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
    1.23    | is_equationlike_term _ = false