# HG changeset patch
# User wenzelm
# Date 1178732238 -7200
# Node ID 1b0f4e6f81aa9ae2b02a47dd86f707d7e2a4c1a0
# Parent  c77a1e1c73234e2f48f85d6af723a6ea72bdffdf
removed unused mk_cond_defpair;

diff -r c77a1e1c7323 -r 1b0f4e6f81aa src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed May 09 19:20:00 2007 +0200
+++ b/src/Pure/logic.ML	Wed May 09 19:37:18 2007 +0200
@@ -45,7 +45,6 @@
   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     term -> (term * term) * term
   val abs_def: term -> term * term
-  val mk_cond_defpair: term list -> term * term -> string * term
   val mk_defpair: term * term -> string * term
   val protectC: term
   val protect: term -> term
@@ -319,14 +318,12 @@
     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   in (lhs', rhs') end;
 
-fun mk_cond_defpair As (lhs, rhs) =
+fun mk_defpair (lhs, rhs) =
   (case Term.head_of lhs of
     Const (name, _) =>
-      (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
+      (NameSpace.base name ^ "_def", 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;
-
 
 
 (** protected propositions and embedded terms **)