src/Pure/logic.ML
changeset 22893 1b0f4e6f81aa
parent 21576 8c11b1ce2f05
child 23238 3de6e253efc4
     1.1 --- a/src/Pure/logic.ML	Wed May 09 19:20:00 2007 +0200
     1.2 +++ b/src/Pure/logic.ML	Wed May 09 19:37:18 2007 +0200
     1.3 @@ -45,7 +45,6 @@
     1.4    val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
     1.5      term -> (term * term) * term
     1.6    val abs_def: term -> term * term
     1.7 -  val mk_cond_defpair: term list -> term * term -> string * term
     1.8    val mk_defpair: term * term -> string * term
     1.9    val protectC: term
    1.10    val protect: term -> term
    1.11 @@ -319,14 +318,12 @@
    1.12      val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
    1.13    in (lhs', rhs') end;
    1.14  
    1.15 -fun mk_cond_defpair As (lhs, rhs) =
    1.16 +fun mk_defpair (lhs, rhs) =
    1.17    (case Term.head_of lhs of
    1.18      Const (name, _) =>
    1.19 -      (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
    1.20 +      (NameSpace.base name ^ "_def", mk_equals (lhs, rhs))
    1.21    | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    1.22  
    1.23 -fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
    1.24 -
    1.25  
    1.26  
    1.27  (** protected propositions and embedded terms **)