# HG changeset patch
# User wenzelm
# Date 974483401 -3600
# Node ID 7b07dd104a1a5ea06e296933aa56794b90475b70
# Parent  f1576723371f699f4ba2ed757583b5ffb516d77b
Envir.beta_norm;

diff -r f1576723371f -r 7b07dd104a1a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Nov 17 18:49:29 2000 +0100
+++ b/src/Pure/thm.ML	Fri Nov 17 18:50:01 2000 +0100
@@ -4,7 +4,7 @@
     Copyright   1994  University of Cambridge
 
 The core of Isabelle's Meta Logic: certified types and terms, meta
-theorems, meta rules (including resolution and simplification).
+theorems, meta rules (including lifting and resolution).
 *)
 
 signature BASIC_THM =
@@ -862,7 +862,7 @@
      maxidx = maxidx,
      shyps = add_term_sorts (t, []),
      hyps = [],
-     prop = Logic.mk_equals (t, if full then Envir.norm_term (Envir.empty 0) t
+     prop = Logic.mk_equals (t, if full then Envir.beta_norm t
        else case t of
           Abs(_, _, bodt) $ u => subst_bound (u, bodt)
         | _ => raise THM ("beta_conversion: not a redex", 0, []))}