# HG changeset patch
# User paulson
# Date 913975246 -3600
# Node ID c4e62bab69bd90c5f1718e91aabc94caf7de6fa2
# Parent  d9fa148383e2e3a8edf36221a37aacadc17b6672
moved dest_eq to hologic.ML and tidied

diff -r d9fa148383e2 -r c4e62bab69bd src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Dec 18 11:00:15 1998 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Fri Dec 18 11:00:46 1998 +0100
@@ -21,14 +21,6 @@
 
 exception RecError of string;
 
-(* FIXME: move? *)
-
-fun dest_eq (Const ("Trueprop", _) $ (Const ("op =", _) $ lhs $ rhs)) = (lhs, rhs)
-  | dest_eq t = raise TERM ("dest_eq", [t])
-
-fun dest_Type (Type x) = x
-  | dest_Type T = raise TYPE ("dest_Type", [T], []);
-
 fun primrec_err s = error ("Primrec definition error:\n" ^ s);
 fun primrec_eq_err sign s eq =
   primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
@@ -37,9 +29,11 @@
 
 fun process_eqn sign (eq, rec_fns) = 
   let
-    val (lhs, rhs) = if null (term_vars eq) then
-        dest_eq eq handle _ => raise RecError "not a proper equation"
-      else raise RecError "illegal schematic variable(s)";
+    val (lhs, rhs) = 
+	if null (term_vars eq) then
+	    HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+	      handle _ => raise RecError "not a proper equation"
+	else raise RecError "illegal schematic variable(s)";
 
     val (recfun, args) = strip_comb lhs;
     val (fname, _) = dest_Const recfun handle _ =>