# HG changeset patch
# User wenzelm
# Date 1164892649 -3600
# Node ID 1af327306c8eeeddb5d3161c579d4fd0503e2c28
# Parent  0fa36ea9aaf5f9b7c20ef0eb748d258c580637c7
added norm/close_result (supercede local_standard etc.);

diff -r 0fa36ea9aaf5 -r 1af327306c8e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Nov 30 14:17:27 2006 +0100
+++ b/src/Pure/goal.ML	Thu Nov 30 14:17:29 2006 +0100
@@ -17,6 +17,8 @@
   val protect: thm -> thm
   val conclude: thm -> thm
   val finish: thm -> thm
+  val norm_result: thm -> thm
+  val close_result: thm -> thm
   val compose_hhf: thm -> int -> thm -> thm Seq.seq
   val compose_hhf_tac: thm -> int -> tactic
   val comp_hhf: thm -> thm -> thm
@@ -77,6 +79,19 @@
 
 (** results **)
 
+(* normal form *)
+
+val norm_result =
+  Drule.flexflex_unique
+  #> MetaSimplifier.norm_hhf_protect
+  #> Thm.strip_shyps
+  #> Drule.zero_var_indexes;
+
+val close_result =
+  Thm.compress
+  #> Drule.close_derivation;
+
+
 (* composition of normal results *)
 
 fun compose_hhf tha i thb =