# HG changeset patch # User wenzelm # Date 1237243184 -3600 # Node ID 0709fda91b06319834c72fe19be24541a1c92076 # Parent 58db562784787dfb56e73b33e85926486ab37a9e refined is_norm_hhf: reject beta-redexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract; diff -r 58db56278478 -r 0709fda91b06 src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Mar 16 23:36:55 2009 +0100 +++ b/src/Pure/drule.ML Mon Mar 16 23:39:44 2009 +0100 @@ -787,14 +787,12 @@ val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq]; -fun is_norm_hhf tm = - let - fun is_norm (Const ("Pure.sort_constraint", _)) = false - | is_norm (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false - | is_norm (t $ u) = is_norm t andalso is_norm u - | is_norm (Abs (_, _, t)) = is_norm t - | is_norm _ = true; - in is_norm (Envir.beta_eta_contract tm) end; +fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false + | is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false + | is_norm_hhf (Abs _ $ _) = false + | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u + | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t + | is_norm_hhf _ = true; fun norm_hhf thy t = if is_norm_hhf t then t