# HG changeset patch
# User wenzelm
# Date 1255733598 -7200
# Node ID 3228627994d94cdcd3f1234148ec11da58a59aed
# Parent  675c0c7e6a37a88b1b813c8cd1ce3ae1e2eb059a
legacy Drule.standard is no longer pervasive;

diff -r 675c0c7e6a37 -r 3228627994d9 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Oct 17 00:52:37 2009 +0200
+++ b/src/Pure/drule.ML	Sat Oct 17 00:53:18 2009 +0200
@@ -29,8 +29,6 @@
   val zero_var_indexes_list: thm list -> thm list
   val zero_var_indexes: thm -> thm
   val implies_intr_hyps: thm -> thm
-  val standard: thm -> thm
-  val standard': thm -> thm
   val rotate_prems: int -> thm -> thm
   val rearrange_prems: int list -> thm -> thm
   val RSN: thm * (int * thm) -> thm
@@ -77,6 +75,8 @@
   val beta_conv: cterm -> cterm -> cterm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val flexflex_unique: thm -> thm
+  val standard: thm -> thm
+  val standard': thm -> thm
   val get_def: theory -> xstring -> thm
   val store_thm: bstring -> thm -> thm
   val store_standard_thm: bstring -> thm -> thm