# 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, []))}