added local_standard;
authorwenzelm
Wed Oct 31 21:59:25 2001 +0100 (2001-10-31)
changeset 12005291593391010
parent 12004 1703de633aaf
child 12006 72fd225a5aa2
added local_standard;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Wed Oct 31 21:59:07 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Oct 31 21:59:25 2001 +0100
     1.3 @@ -99,6 +99,7 @@
     1.4    val has_internal: tag list -> bool
     1.5    val impose_hyps: cterm list -> thm -> thm
     1.6    val close_derivation: thm -> thm
     1.7 +  val local_standard: thm -> thm
     1.8    val compose_single: thm * int * thm -> thm
     1.9    val add_rules: thm list -> thm list -> thm list
    1.10    val del_rules: thm list -> thm list -> thm list
    1.11 @@ -365,6 +366,10 @@
    1.12  
    1.13  val standard = close_derivation o standard';
    1.14  
    1.15 +fun local_standard th =
    1.16 +  th |> strip_shyps_warning |> zero_var_indexes
    1.17 +  |> Thm.compress |> close_derivation;
    1.18 +
    1.19  
    1.20  (*Convert all Vars in a theorem to Frees.  Also return a function for
    1.21    reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.