# HG changeset patch
# User wenzelm
# Date 1011297586 -3600
# Node ID 95bfef18da83b40e84ebf11b83e31736f830c72c
# Parent  fc716621f19d5419e515e387a10cb548cfe70e99
is_norm_hhf moved to drule.ML;

diff -r fc716621f19d -r 95bfef18da83 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Jan 17 20:59:31 2002 +0100
+++ b/src/Pure/logic.ML	Thu Jan 17 20:59:46 2002 +0100
@@ -47,7 +47,6 @@
   val strip_assums_hyp  : term -> term list
   val strip_assums_concl: term -> term
   val strip_params      : term -> (string * typ) list
-  val is_norm_hhf       : term -> bool
   val has_meta_prems    : term -> int -> bool
   val flatten_params    : int -> term -> term
   val auto_rename       : bool ref
@@ -264,12 +263,6 @@
   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   | strip_params B = [];
 
-(*test for HHF normal form*)
-fun is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = 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;
-
 (*test for meta connectives in prems of a 'subgoal'*)
 fun has_meta_prems prop i =
   let