# HG changeset patch
# User wenzelm
# Date 1027462316 -7200
# Node ID 15597d5020356646ff5e1bb11c3a276044bfe052
# Parent  0b60b9e18a26fa9d0aa984ff6ba6f0052d9fc0be
removed attribute "norm_hhf";

diff -r 0b60b9e18a26 -r 15597d502035 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Jul 24 00:11:24 2002 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Jul 24 00:11:56 2002 +0200
@@ -288,7 +288,6 @@
 (* misc rules *)
 
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
-fun norm_hhf x = no_args (Drule.rule_attribute (K Tactic.norm_hhf_rule)) x;
 fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
 fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
 
@@ -342,7 +341,6 @@
   ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
   ("folded", (folded_global, folded_local), "folded definitions"),
   ("standard", (standard, standard), "result put into standard form"),
-  ("norm_hhf", (norm_hhf, norm_hhf), "result put into HHF normal form"),
   ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
   ("no_vars", (no_vars, no_vars), "frozen schematic vars"),
   ("consumes", (consumes, consumes), "number of consumed facts"),