# HG changeset patch
# User berghofe
# Date 1077036090 -3600
# Node ID bb726050650d060933a3fea7e4885a60814e6ece
# Parent  55fe71faaddafb538f1f447269ac5bb80d8d0681
Moved application of flexflex_unique from standard' to standard.

diff -r 55fe71faadda -r bb726050650d src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Feb 17 10:41:59 2004 +0100
+++ b/src/Pure/drule.ML	Tue Feb 17 17:41:30 2004 +0100
@@ -384,13 +384,13 @@
 fun standard' th =
   let val {maxidx,...} = rep_thm th in
     th
-    |> flexflex_unique |> implies_intr_hyps 
+    |> implies_intr_hyps
     |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
     |> strip_shyps_warning
     |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   end;
 
-val standard = close_derivation o standard';
+val standard = close_derivation o standard' o flexflex_unique;
 
 fun local_standard th =
   th |> strip_shyps |> zero_var_indexes