--- 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;