1.1 --- a/src/Pure/goal.ML	Thu Nov 30 14:17:27 2006 +0100
     1.2 +++ b/src/Pure/goal.ML	Thu Nov 30 14:17:29 2006 +0100
     1.3 @@ -17,6 +17,8 @@
     1.4    val protect: thm -> thm
     1.5    val conclude: thm -> thm
     1.6    val finish: thm -> thm
     1.7 +  val norm_result: thm -> thm
     1.8 +  val close_result: thm -> thm
     1.9    val compose_hhf: thm -> int -> thm -> thm Seq.seq
    1.10    val compose_hhf_tac: thm -> int -> tactic
    1.11    val comp_hhf: thm -> thm -> thm
    1.12 @@ -77,6 +79,19 @@
    1.13  
    1.14  (** results **)
    1.15  
    1.16 +(* normal form *)
    1.17 +
    1.18 +val norm_result =
    1.19 +  Drule.flexflex_unique
    1.20 +  #> MetaSimplifier.norm_hhf_protect
    1.21 +  #> Thm.strip_shyps
    1.22 +  #> Drule.zero_var_indexes;
    1.23 +
    1.24 +val close_result =
    1.25 +  Thm.compress
    1.26 +  #> Drule.close_derivation;
    1.27 +
    1.28 +
    1.29  (* composition of normal results *)
    1.30  
    1.31  fun compose_hhf tha i thb =