# HG changeset patch
# User wenzelm
# Date 1002881284 -7200
# Node ID a7da2e8b5762592ed8aa28776e22a8f3e3967dd1
# Parent  b5f6963b193c04cdf4a239ccee942b36a7bcf83f
removed read_inst', no longer export insts';

diff -r b5f6963b193c -r a7da2e8b5762 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;