src/HOL/Library/simps_case_conv.ML
changeset 56252 b72e0a9d62b9
parent 55997 9dc5ce83202c
child 57628 c80fc5576271
     1.1 --- a/src/HOL/Library/simps_case_conv.ML	Sat Mar 22 18:12:08 2014 +0100
     1.2 +++ b/src/HOL/Library/simps_case_conv.ML	Sat Mar 22 18:15:09 2014 +0100
     1.3 @@ -152,13 +152,12 @@
     1.4  
     1.5  fun was_split t =
     1.6    let
     1.7 -    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
     1.8 -              o fst o HOLogic.dest_imp
     1.9 +    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
    1.10      val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
    1.11 -    fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
    1.12 +    fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
    1.13        | dest_alls t = t
    1.14    in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
    1.15 -        handle TERM _ => false
    1.16 +  handle TERM _ => false
    1.17  
    1.18  fun apply_split ctxt split thm = Seq.of_list
    1.19    let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in