# HG changeset patch
# User paulson
# Date 1100539294 -3600
# Node ID 9d49290ed885822f196abb44a33bf2dd88bb2134
# Parent  55b7f79206228e8f13984c4023391bd886dae959
removed a "clone" (duplicate code)

diff -r 55b7f7920622 -r 9d49290ed885 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Nov 15 17:04:11 2004 +0100
+++ b/src/HOL/HOL.thy	Mon Nov 15 18:21:34 2004 +0100
@@ -1001,6 +1001,27 @@
    class for quasi orders, the tactics Quasi_Tac.trans_tac and
    Quasi_Tac.quasi_tac are not of much use. *)
 
+fun decomp_gen sort sign (Trueprop $ t) =
+  let fun of_sort t = Sign.of_sort sign (type_of t, sort)
+  fun dec (Const ("Not", _) $ t) = (
+	  case dec t of
+	    None => None
+	  | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
+	| dec (Const ("op =",  _) $ t1 $ t2) = 
+	    if of_sort t1
+	    then Some (t1, "=", t2)
+	    else None
+	| dec (Const ("op <=",  _) $ t1 $ t2) = 
+	    if of_sort t1
+	    then Some (t1, "<=", t2)
+	    else None
+	| dec (Const ("op <",  _) $ t1 $ t2) = 
+	    if of_sort t1
+	    then Some (t1, "<", t2)
+	    else None
+	| dec _ = None
+  in dec t end;
+
 structure Quasi_Tac = Quasi_Tac_Fun (
   struct
     val le_trans = thm "order_trans";
@@ -1012,28 +1033,6 @@
     val le_neq_trans = thm "order_le_neq_trans";
     val neq_le_trans = thm "order_neq_le_trans";
     val less_imp_neq = thm "less_imp_neq";
-
-    fun decomp_gen sort sign (Trueprop $ t) =
-      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
-      fun dec (Const ("Not", _) $ t) = (
-              case dec t of
-                None => None
-              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
-            | dec (Const ("op =",  _) $ t1 $ t2) = 
-                if of_sort t1
-                then Some (t1, "=", t2)
-                else None
-            | dec (Const ("op <=",  _) $ t1 $ t2) = 
-                if of_sort t1
-                then Some (t1, "<=", t2)
-                else None
-            | dec (Const ("op <",  _) $ t1 $ t2) = 
-                if of_sort t1
-                then Some (t1, "<", t2)
-                else None
-            | dec _ = None
-      in dec t end;
-
     val decomp_trans = decomp_gen ["HOL.order"];
     val decomp_quasi = decomp_gen ["HOL.order"];
 
@@ -1059,28 +1058,6 @@
     val neq_le_trans = thm "order_neq_le_trans";
     val less_imp_neq = thm "less_imp_neq";
     val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
-
-    fun decomp_gen sort sign (Trueprop $ t) =
-      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
-      fun dec (Const ("Not", _) $ t) = (
-              case dec t of
-                None => None
-              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
-            | dec (Const ("op =",  _) $ t1 $ t2) = 
-                if of_sort t1
-                then Some (t1, "=", t2)
-                else None
-            | dec (Const ("op <=",  _) $ t1 $ t2) = 
-                if of_sort t1
-                then Some (t1, "<=", t2)
-                else None
-            | dec (Const ("op <",  _) $ t1 $ t2) = 
-                if of_sort t1
-                then Some (t1, "<", t2)
-                else None
-            | dec _ = None
-      in dec t end;
-
     val decomp_part = decomp_gen ["HOL.order"];
     val decomp_lin = decomp_gen ["HOL.linorder"];