# HG changeset patch
# User wenzelm
# Date 1303478640 -7200
# Node ID 1805c67dc7aab1e2f78f428669fc2e8b363e8f78
# Parent  38b9f023cc34330f75d36a6f0024a3e007239ffd
simplified Data signature;

diff -r 38b9f023cc34 -r 1805c67dc7aa src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Apr 22 15:05:04 2011 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 22 15:24:00 2011 +0200
@@ -55,12 +55,12 @@
 structure Quantifier1 = Quantifier1
 (
   (*abstract syntax*)
-  fun dest_eq((c as Const(@{const_name eq},_)) $ s $ t) = SOME(c,s,t)
-    | dest_eq _ = NONE;
-  fun dest_conj((c as Const(@{const_name conj},_)) $ s $ t) = SOME(c,s,t)
-    | dest_conj _ = NONE;
-  fun dest_imp((c as Const(@{const_name imp},_)) $ s $ t) = SOME(c,s,t)
-    | dest_imp _ = NONE;
+  fun dest_eq (Const (@{const_name eq}, _) $ s $ t) = SOME (s, t)
+    | dest_eq _ = NONE
+  fun dest_conj (Const (@{const_name conj}, _) $ s $ t) = SOME (s, t)
+    | dest_conj _ = NONE
+  fun dest_imp (Const (@{const_name imp}, _) $ s $ t) = SOME (s, t)
+    | dest_imp _ = NONE
   val conj = FOLogic.conj
   val imp  = FOLogic.imp
   (*rules*)
diff -r 38b9f023cc34 -r 1805c67dc7aa src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 15:05:04 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 15:24:00 2011 +0200
@@ -10,11 +10,11 @@
 structure Quantifier1 = Quantifier1
 (
   (*abstract syntax*)
-  fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
+  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
     | dest_eq _ = NONE;
-  fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
+  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
     | dest_conj _ = NONE;
-  fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
+  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
     | dest_imp _ = NONE;
   val conj = HOLogic.conj
   val imp  = HOLogic.imp
diff -r 38b9f023cc34 -r 1805c67dc7aa src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Fri Apr 22 15:05:04 2011 +0200
+++ b/src/Provers/quantifier1.ML	Fri Apr 22 15:24:00 2011 +0200
@@ -40,9 +40,9 @@
 signature QUANTIFIER1_DATA =
 sig
   (*abstract syntax*)
-  val dest_eq: term -> (term * term * term) option
-  val dest_conj: term -> (term * term * term) option
-  val dest_imp: term -> (term * term * term) option
+  val dest_eq: term -> (term * term) option
+  val dest_conj: term -> (term * term) option
+  val dest_imp: term -> (term * term) option
   val conj: term
   val imp: term
   (*rules*)
@@ -79,7 +79,7 @@
 (* FIXME: only test! *)
 fun def xs eq =
   (case Data.dest_eq eq of
-    SOME (c, s, t) =>
+    SOME (s, t) =>
       let val n = length xs in
         s = Bound n andalso not (loose_bvar1 (t, n)) orelse
         t = Bound n andalso not (loose_bvar1 (s, n))
@@ -89,7 +89,7 @@
 fun extract_conj fst xs t =
   (case Data.dest_conj t of
     NONE => NONE
-  | SOME (conj, P, Q) =>
+  | SOME (P, Q) =>
       if def xs P then (if fst then NONE else SOME (xs, P, Q))
       else if def xs Q then SOME (xs, Q, P)
       else
@@ -103,7 +103,7 @@
 fun extract_imp fst xs t =
   (case Data.dest_imp t of
     NONE => NONE
-  | SOME (imp, P, Q) =>
+  | SOME (P, Q) =>
       if def xs P then (if fst then NONE else SOME (xs, P, Q))
       else
         (case extract_conj false xs P of
@@ -115,7 +115,7 @@
 
 fun extract_quant extract q =
   let
-    fun exqu xs ((qC as Const(qa, _)) $ Abs (x, T, Q)) =
+    fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) =
           if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
       | exqu xs P = extract (null xs) xs P
   in exqu [] end;
@@ -225,3 +225,4 @@
   | _ => NONE);
 
 end;
+