dest_def: actually return beta-eta contracted equation;
authorwenzelm
Thu Feb 16 18:25:55 2006 +0100 (2006-02-16)
changeset 19071fdffd7c40864
parent 19070 99001616e0e2
child 19072 946ef711dc7d
dest_def: actually return beta-eta contracted equation;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Thu Feb 16 18:25:54 2006 +0100
     1.2 +++ b/src/Pure/logic.ML	Thu Feb 16 18:25:55 2006 +0100
     1.3 @@ -206,13 +206,15 @@
     1.4  fun dest_def pp check_head is_fixed is_fixedT eq =
     1.5    let
     1.6      fun err msg = raise TERM (msg, [eq]);
     1.7 -    val bound_vars = Syntax.bound_vars (Term.strip_all_vars eq);
     1.8 -    val display_terms = commas_quote o map (Pretty.string_of_term pp o bound_vars);
     1.9 +    val eq_vars = Term.strip_all_vars eq;
    1.10 +    val eq_body = Term.strip_all_body eq;
    1.11 +
    1.12 +    val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
    1.13      val display_types = commas_quote o map (Pretty.string_of_typ pp);
    1.14  
    1.15 -    val (lhs, rhs) = dest_equals (Term.strip_all_body eq)
    1.16 -      handle TERM _ => err "Not a meta-equality (==)";
    1.17 -    val (head, args) = Term.strip_comb (Envir.beta_eta_contract lhs);
    1.18 +    val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
    1.19 +    val lhs = Envir.beta_eta_contract raw_lhs;
    1.20 +    val (head, args) = Term.strip_comb lhs;
    1.21      val head_tfrees = Term.add_tfrees head [];
    1.22  
    1.23      fun check_arg (Bound _) = true
    1.24 @@ -243,7 +245,7 @@
    1.25        err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
    1.26      else if exists_subterm (fn t => t aconv head) rhs then
    1.27        err "Entity to be defined occurs on rhs"
    1.28 -    else ((lhs, rhs), fold_rev close_arg args eq)
    1.29 +    else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs)))))
    1.30    end;
    1.31  
    1.32  (*!!x. c x == t[x] to c == %x. t[x]*)