src/Pure/Isar/attrib.ML

   val local_thms: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
   val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
   val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
   val no_args: 'a attribute -> Args.src -> 'a attribute
   val add_del_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
-  val read_inst': string option list * string option list -> ProofContext.context -> thm -> thm
-  val insts': Args.T list -> (string option list * string option list) * Args.T list
   val setup: (theory -> theory) list
 end;
 
 structure Attrib: ATTRIB =
 struct

       in
         thm
         |> read_instantiate context_of insts x
         |> RuleCases.save thm
       end;
-
-val read_inst' = read_instantiate' I;
 
 val concl = Args.$$$ "concl" -- Args.colon;
 val inst_arg = Scan.unless concl Args.name_dummy;
 val inst_args = Scan.repeat inst_arg;
 fun insts' x = (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x;