# HG changeset patch
# User berghofe
# Date 1235662366 -3600
# Node ID f3b3b0e3d1844e7659048e7fc71b703f983a92d3
# Parent  896fed07349e83750bcf3562fb9038fd31805854
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
in case assumptions are not of the form (Trueprop $ ...).

diff -r 896fed07349e -r f3b3b0e3d184 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Feb 25 11:30:46 2009 -0800
+++ b/src/HOL/Orderings.thy	Thu Feb 26 16:32:46 2009 +0100
@@ -331,7 +331,7 @@
 
 fun struct_tac ((s, [eq, le, less]), thms) prems =
   let
-    fun decomp thy (Trueprop $ t) =
+    fun decomp thy (@{const Trueprop} $ t) =
       let
         fun excluded t =
           (* exclude numeric types: linear arithmetic subsumes transitivity *)
@@ -350,7 +350,8 @@
 	      of NONE => NONE
 	       | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
           | dec x = rel x;
-      in dec t end;
+      in dec t end
+      | decomp thy _ = NONE;
   in
     case s of
       "order" => Order_Tac.partial_tac decomp thms prems
diff -r 896fed07349e -r f3b3b0e3d184 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Feb 25 11:30:46 2009 -0800
+++ b/src/HOL/Transitive_Closure.thy	Thu Feb 26 16:32:46 2009 +0100
@@ -646,7 +646,7 @@
     val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
     val rtrancl_trans = @{thm rtrancl_trans};
 
-  fun decomp (Trueprop $ t) =
+  fun decomp (@{const Trueprop} $ t) =
     let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
         let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
               | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
@@ -654,7 +654,8 @@
             val (rel,r) = decr (Envir.beta_eta_contract rel);
         in SOME (a,b,rel,r) end
       | dec _ =  NONE
-    in dec t end;
+    in dec t end
+    | decomp _ = NONE;
 
   end);
 
@@ -669,7 +670,7 @@
     val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
     val rtrancl_trans = @{thm rtranclp_trans};
 
-  fun decomp (Trueprop $ t) =
+  fun decomp (@{const Trueprop} $ t) =
     let fun dec (rel $ a $ b) =
         let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
               | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
@@ -677,7 +678,8 @@
             val (rel,r) = decr rel;
         in SOME (a, b, rel, r) end
       | dec _ =  NONE
-    in dec t end;
+    in dec t end
+    | decomp _ = NONE;
 
   end);
 *}