# HG changeset patch
# User wenzelm
# Date 1331634159 -3600
# Node ID de5cfda8b2de83f9dbf5b826455d7ee0b4d96860
# Parent  e2ad717ec889d98a33d9a8e0bda7ee31e27b3dcd
tuned strip_alls;

diff -r e2ad717ec889 -r de5cfda8b2de src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 11:21:26 2012 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 11:22:39 2012 +0100
@@ -253,7 +253,9 @@
                     ^ ML_Syntax.print_term pat)
 
 fun strip_alls t =
-  if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t
+  (case try Logic.dest_all t of
+    SOME (_, u) => strip_alls u
+  | NONE => t)
 
 fun compile_eq match_name eq =
   let
@@ -293,9 +295,7 @@
   let
     val tab = FixrecUnfoldData.get (Context.Proof ctxt)
     val ss = Simplifier.simpset_of ctxt
-    fun concl t =
-      if Logic.is_all t then concl (snd (Logic.dest_all t))
-      else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
+    val concl = HOLogic.dest_Trueprop o Logic.strip_imp_concl o strip_alls
     fun tac (t, i) =
       let
         val (c, _) =