src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Fri Oct 12 12:07:27 2001 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Oct 12 12:08:04 2001 +0200
@@ -33,8 +33,6 @@
   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;
 
@@ -251,8 +249,6 @@
         |> 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;