--- 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.