# HG changeset patch
# User wenzelm
# Date 893264929 -7200
# Node ID 2733e21814fe21e2db4cdcb40e68444cce792600
# Parent  bfbaea156f43cf1157ddd567adf76e502dd449b2
added mk_cond_defpair, mk_defpair;

diff -r bfbaea156f43 -r 2733e21814fe src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Apr 22 14:06:05 1998 +0200
+++ b/src/Pure/logic.ML	Wed Apr 22 19:08:49 1998 +0200
@@ -26,6 +26,8 @@
   val list_flexpairs	: (term*term)list * term -> term
   val list_implies	: term list * term -> term
   val list_rename_params: string list * term -> term
+  val mk_cond_defpair	: term list -> term * term -> string * term
+  val mk_defpair	: term * term -> string * term
   val mk_equals		: term * term -> term
   val mk_flexpair	: term * term -> term
   val mk_implies	: term * term -> term
@@ -72,6 +74,7 @@
 fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
   | dest_implies A = raise TERM("dest_implies", [A]);
 
+
 (** nested implications **)
 
 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
@@ -98,6 +101,7 @@
 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   | count_prems (_,n) = n;
 
+
 (** flex-flex constraints **)
 
 (*Make a constraint.*)
@@ -136,6 +140,18 @@
   let val (tpairs,horn) = strip_flexpairs A 
   in  (tpairs, strip_imp_prems horn, strip_imp_concl horn)   end;
 
+
+(** definitions **)
+
+fun mk_cond_defpair As (lhs, rhs) =
+  (case Term.head_of lhs of
+    Const (name, _) =>
+      (Sign.base_name name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
+  | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
+
+fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
+
+
 (** types as terms **)
 
 fun mk_type ty = Const ("TYPE", itselfT ty);
@@ -143,6 +159,7 @@
 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   | dest_type t = raise TERM ("dest_type", [t]);
 
+
 (** class constraints **)
 
 fun mk_inclass (ty, c) =