# HG changeset patch
# User wenzelm
# Date 1004561965 -3600
# Node ID 29159339101018c35d4d199df487972dc6b8ba1c
# Parent  1703de633aaf5771dd2066563b6c849cdf012958
added local_standard;

diff -r 1703de633aaf -r 291593391010 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Oct 31 21:59:07 2001 +0100
+++ b/src/Pure/drule.ML	Wed Oct 31 21:59:25 2001 +0100
@@ -99,6 +99,7 @@
   val has_internal: tag list -> bool
   val impose_hyps: cterm list -> thm -> thm
   val close_derivation: thm -> thm
+  val local_standard: thm -> thm
   val compose_single: thm * int * thm -> thm
   val add_rules: thm list -> thm list -> thm list
   val del_rules: thm list -> thm list -> thm list
@@ -365,6 +366,10 @@
 
 val standard = close_derivation o standard';
 
+fun local_standard th =
+  th |> strip_shyps_warning |> zero_var_indexes
+  |> Thm.compress |> close_derivation;
+
 
 (*Convert all Vars in a theorem to Frees.  Also return a function for
   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.