# HG changeset patch
# User wenzelm
# Date 1011297876 -3600
# Node ID 163a85ba885b0bc58281920aff0816f8b553c937
# Parent  37131c76dff6cbc1b732574d7f640dab4bf788f0
Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;

diff -r 37131c76dff6 -r 163a85ba885b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jan 17 21:04:16 2002 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Jan 17 21:04:36 2002 +0100
@@ -241,7 +241,7 @@
           | zip_vars ((x, _) :: xs) (Some t :: opt_ts) = (x, t) :: zip_vars xs opt_ts
           | zip_vars [] _ = error "More instantiations than variables in theorem";
         val insts =
-          zip_vars (Drule.vars_of_terms [#prop (Thm.rep_thm thm)]) args @
+          zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
           zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
       in
         thm
@@ -288,7 +288,7 @@
 (* 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)) 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;
 
diff -r 37131c76dff6 -r 163a85ba885b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jan 17 21:04:16 2002 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Jan 17 21:04:36 2002 +0100
@@ -652,7 +652,7 @@
 fun pretty_thm ctxt thm =
   if ! Display.show_hyps then
     Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm
-  else pretty_term ctxt (#prop (Thm.rep_thm thm));
+  else pretty_term ctxt (Thm.prop_of thm);
 
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
@@ -724,7 +724,7 @@
     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   in fn thm => thm
-    |> Tactic.norm_hhf
+    |> Tactic.norm_hhf_rule
     |> Seq.EVERY (rev exp_asms)
     |> Seq.map (fn rule =>
       let
@@ -734,7 +734,7 @@
       in
         rule
         |> Drule.forall_intr_list frees
-        |> Tactic.norm_hhf
+        |> Tactic.norm_hhf_rule
         |> (#1 o Drule.tvars_intr_list tfrees)
       end)
   end;
@@ -1038,7 +1038,7 @@
 fun add_assm (ctxt, ((name, attrs), props)) =
   let
     val cprops = map (Thm.cterm_of (sign_of ctxt)) props;
-    val asms = map (Tactic.norm_hhf o Thm.assume) cprops;
+    val asms = map (Tactic.norm_hhf_rule o Thm.assume) cprops;
 
     val ths = map (fn th => ([th], [])) asms;
     val (ctxt', [(_, thms)]) =