diff -r df377a6fdd90 -r 56d2c357e6b5 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 20 14:48:04 2015 +0100
@@ -4,8 +4,15 @@
 Rule instantiations -- operations within implicit rule / subgoal context.
 *)
 
-signature BASIC_RULE_INSTS =
+signature RULE_INSTS =
 sig
+  val where_rule: Proof.context ->
+    ((indexname * Position.T) * string) list ->
+    (binding * string option * mixfix) list -> thm -> thm
+  val of_rule: Proof.context -> string option list * string option list ->
+    (binding * string option * mixfix) list -> thm -> thm
+  val read_instantiate: Proof.context ->
+    ((indexname * Position.T) * string) list -> string list -> thm -> thm
   val res_inst_tac: Proof.context ->
     ((indexname * Position.T) * string) list -> thm -> int -> tactic
   val eres_inst_tac: Proof.context ->
@@ -18,18 +25,6 @@
     ((indexname * Position.T) * string) list -> thm -> int -> tactic
   val thin_tac: Proof.context -> string -> int -> tactic
   val subgoal_tac: Proof.context -> string -> int -> tactic
-end;
-
-signature RULE_INSTS =
-sig
-  include BASIC_RULE_INSTS
-  val where_rule: Proof.context ->
-    ((indexname * Position.T) * string) list ->
-    (binding * string option * mixfix) list -> thm -> thm
-  val of_rule: Proof.context -> string option list * string option list ->
-    (binding * string option * mixfix) list -> thm -> thm
-  val read_instantiate: Proof.context ->
-    ((indexname * Position.T) * string) list -> string list -> thm -> thm
   val make_elim_preserve: Proof.context -> thm -> thm
   val method:
     (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) ->
@@ -346,6 +341,3 @@
       "remove premise (dynamic instantiation)");
 
 end;
-
-structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
-open Basic_Rule_Insts;