# HG changeset patch
# User wenzelm
# Date 1213200194 -7200
# Node ID e9f2d5947887ba857a4ea77a531d175579ccf118
# Parent  30e3bdfbbef1160f65b53f3bdf44c35b17a63d40
qualified types_sorts, read_insts etc.;

diff -r 30e3bdfbbef1 -r e9f2d5947887 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jun 11 18:02:50 2008 +0200
+++ b/src/Pure/drule.ML	Wed Jun 11 18:03:14 2008 +0200
@@ -17,10 +17,6 @@
   val cprems_of: thm -> cterm list
   val cterm_fun: (term -> term) -> (cterm -> cterm)
   val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
-  val read_insts: theory -> (indexname -> typ option) * (indexname -> sort option) ->
-    (indexname -> typ option) * (indexname -> sort option) -> string list ->
-    (indexname * string) list -> (ctyp * ctyp) list * (cterm * cterm) list
-  val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val forall_intr_list: cterm list -> thm -> thm
   val forall_intr_frees: thm -> thm
   val forall_intr_vars: thm -> thm
@@ -50,8 +46,6 @@
   val COMP: thm * thm -> thm
   val INCR_COMP: thm * thm -> thm
   val COMP_INCR: thm * thm -> thm
-  val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
-  val read_instantiate: (string*string)list -> thm -> thm
   val cterm_instantiate: (cterm*cterm)list -> thm -> thm
   val size_of_thm: thm -> int
   val reflexive_thm: thm
@@ -83,6 +77,10 @@
   val strip_comb: cterm -> cterm * cterm list
   val strip_type: ctyp -> ctyp list * ctyp
   val beta_conv: cterm -> cterm -> cterm
+  val read_insts: theory -> (indexname -> typ option) * (indexname -> sort option) ->
+    (indexname -> typ option) * (indexname -> sort option) -> string list ->
+    (indexname * string) list -> (ctyp * ctyp) list * (cterm * cterm) list
+  val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val add_used: thm -> string list -> string list
   val flexflex_unique: thm -> thm
   val store_thm: bstring -> thm -> thm
@@ -105,6 +103,10 @@
   val protectI: thm
   val protectD: thm
   val protect_cong: thm
+  val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
+  val read_instantiate: (string*string)list -> thm -> thm
+  val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
+  val read_instantiate': (indexname * string) list -> thm -> thm
   val implies_intr_protected: cterm list -> thm -> thm
   val termI: thm
   val mk_term: cterm -> thm
@@ -124,8 +126,6 @@
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
   val abs_def: thm -> thm
-  val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
-  val read_instantiate': (indexname * string) list -> thm -> thm
 end;
 
 structure Drule: DRULE =