1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 11:21:26 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 11:22:39 2012 +0100
     1.3 @@ -253,7 +253,9 @@
     1.4                      ^ ML_Syntax.print_term pat)
     1.5  
     1.6  fun strip_alls t =
     1.7 -  if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t
     1.8 +  (case try Logic.dest_all t of
     1.9 +    SOME (_, u) => strip_alls u
    1.10 +  | NONE => t)
    1.11  
    1.12  fun compile_eq match_name eq =
    1.13    let
    1.14 @@ -293,9 +295,7 @@
    1.15    let
    1.16      val tab = FixrecUnfoldData.get (Context.Proof ctxt)
    1.17      val ss = Simplifier.simpset_of ctxt
    1.18 -    fun concl t =
    1.19 -      if Logic.is_all t then concl (snd (Logic.dest_all t))
    1.20 -      else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
    1.21 +    val concl = HOLogic.dest_Trueprop o Logic.strip_imp_concl o strip_alls
    1.22      fun tac (t, i) =
    1.23        let
    1.24          val (c, _) =