--- 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
--- 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'))
--- 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))))
--- 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' [];
--- 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;
--- 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;