# HG changeset patch
# User wenzelm
# Date 1139255934 -3600
# Node ID d8143510868898a91879328c3e1f9b549ffdcdb6
# Parent  042608ffa2ece2ecd4d755cf56684a3f850f5e95
Envir.(beta_)eta_contract;

diff -r 042608ffa2ec -r d81435108688 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon Feb 06 11:01:28 2006 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Mon Feb 06 20:58:54 2006 +0100
@@ -1052,9 +1052,9 @@
 
 fun rearrange sg tm th =
     let
-	val tm' = Pattern.beta_eta_contract tm
+	val tm' = Envir.beta_eta_contract tm
 	fun find []      n = permute_prems 0 1 0 (implies_intr (Thm.cterm_of sg tm) th)
-	  | find (p::ps) n = if tm' aconv (Pattern.beta_eta_contract p)
+	  | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
 			     then permute_prems n 1 0 th
 			     else find ps (n+1)
     in
diff -r 042608ffa2ec -r d81435108688 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Mon Feb 06 11:01:28 2006 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Feb 06 20:58:54 2006 +0100
@@ -72,7 +72,7 @@
                   val rT = List.nth (rec_result_Ts, i);
                   val vs' = filter_out is_unit vs;
                   val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
-                  val f' = Pattern.eta_contract (list_abs_free
+                  val f' = Envir.eta_contract (list_abs_free
                     (map dest_Free vs, if i mem is then list_comb (f, vs')
                       else HOLogic.unit));
                 in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
diff -r 042608ffa2ec -r d81435108688 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Feb 06 11:01:28 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Feb 06 20:58:54 2006 +0100
@@ -336,7 +336,7 @@
         end
       else ((recs, dummies), replicate (length rs) Extraction.nullt))
         ((get #rec_thms dt_info, dummies), rss);
-    val rintrs = map (fn (intr, c) => Pattern.eta_contract
+    val rintrs = map (fn (intr, c) => Envir.eta_contract
       (Extraction.realizes_of thy2 vs
         c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
           (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
diff -r 042608ffa2ec -r d81435108688 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Feb 06 11:01:28 2006 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Mon Feb 06 20:58:54 2006 +0100
@@ -326,7 +326,7 @@
   | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 _ _ = error "prop_of: partial proof object";
 
-val prop_of' = Pattern.eta_contract oo (Envir.beta_norm oo prop_of0);
+val prop_of' = Envir.beta_eta_contract oo prop_of0;
 val prop_of = prop_of' [];
 
 
diff -r 042608ffa2ec -r d81435108688 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Feb 06 11:01:28 2006 +0100
+++ b/src/Pure/drule.ML	Mon Feb 06 20:58:54 2006 +0100
@@ -854,7 +854,7 @@
       | is_norm (t $ u) = is_norm t andalso is_norm u
       | is_norm (Abs (_, _, t)) = is_norm t
       | is_norm _ = true;
-  in is_norm (Pattern.beta_eta_contract tm) end;
+  in is_norm (Envir.beta_eta_contract tm) end;
 
 fun norm_hhf thy t =
   if is_norm_hhf t then t
@@ -1012,7 +1012,7 @@
     fun rename [] t = ([], t)
       | rename (x' :: xs) (Abs (x, T, t)) =
           let val (xs', t') = rename xs t
-          in (xs', Abs (getOpt (x',x), T, t')) end
+          in (xs', Abs (the_default x x', T, t')) end
       | rename xs (t $ u) =
           let
             val (xs', t') = rename xs t;
diff -r 042608ffa2ec -r d81435108688 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Feb 06 11:01:28 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Mon Feb 06 20:58:54 2006 +0100
@@ -430,7 +430,7 @@
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
     val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
-    val erhs = Pattern.eta_contract (term_of rhs);
+    val erhs = Envir.eta_contract (term_of rhs);
     val perm =
       var_perm (term_of elhs, erhs) andalso
       not (term_of elhs aconv erhs) andalso
@@ -551,7 +551,7 @@
     let
       val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
-    (*val lhs = Pattern.eta_contract lhs;*)
+    (*val lhs = Envir.eta_contract lhs;*)
       val a = valOf (cong_name (head_of (term_of lhs))) handle Option =>
         raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
       val (alist, weak) = congs;
@@ -565,7 +565,7 @@
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
         raise SIMPLIFIER ("Congruence not a meta-equality", thm);
-    (*val lhs = Pattern.eta_contract lhs;*)
+    (*val lhs = Envir.eta_contract lhs;*)
       val a = valOf (cong_name (head_of lhs)) handle Option =>
         raise SIMPLIFIER ("Congruence must start with a constant", thm);
       val (alist, _) = congs;