# HG changeset patch
# User wenzelm
# Date 978812884 -3600
# Node ID ae001d5119fc1122c205d6d0c8de31bea77fb69f
# Parent  2eba1c06592cab4853da4bc39b73ad1e0bc880a0
export read_inst', inst';
tuned;

diff -r 2eba1c06592c -r ae001d5119fc src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Jan 06 21:27:33 2001 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Jan 06 21:28:04 2001 +0100
@@ -33,6 +33,8 @@
   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;
 
@@ -197,26 +199,31 @@
 
 (* where: named instantiations *)
 
-fun read_instantiate context_of insts x thm =
-  let
-    val ctxt = context_of x;
-    val sign = ProofContext.sign_of ctxt;
+fun read_instantiate _ [] _ thm = thm
+  | read_instantiate context_of insts x thm =
+      let
+        val ctxt = context_of x;
+        val sign = ProofContext.sign_of ctxt;
+
+        val vars = Drule.vars_of thm;
+        fun get_typ xi =
+          (case assoc (vars, xi) of
+            Some T => T
+          | None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi));
 
-    val vars = Drule.vars_of thm;
-    fun get_typ xi =
-      (case assoc (vars, xi) of
-        Some T => T
-      | None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi));
+        val (xs, ss) = Library.split_list insts;
+        val Ts = map get_typ xs;
 
-    val (xs, ss) = Library.split_list insts;
-    val Ts = map get_typ xs;
-
-    val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts);
-    val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
-    val cenv =
-      map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
-        (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
-  in Drule.instantiate (cenvT, cenv) thm end;
+        val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts);
+        val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
+        val cenv =
+          map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
+            (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
+      in
+        thm
+        |> Drule.instantiate (cenvT, cenv)
+        |> RuleCases.save thm
+      end;
 
 fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x;
 
@@ -228,23 +235,31 @@
 
 (* of: positional instantiations *)
 
-fun read_instantiate' context_of (args, concl_args) x thm =
-  let
-    fun zip_vars _ [] = []
-      | zip_vars (_ :: xs) (None :: opt_ts) = zip_vars xs opt_ts
-      | zip_vars ((x, _) :: xs) (Some t :: opt_ts) = (x, t) :: zip_vars xs opt_ts
-      | zip_vars [] _ = error "More instantiations than variables in theorem";
-    val insts =
-      zip_vars (Drule.vars_of_terms [#prop (Thm.rep_thm thm)]) args @
-      zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
-  in read_instantiate context_of insts x thm end;
+fun read_instantiate' _ ([], []) _ thm = thm
+  | read_instantiate' context_of (args, concl_args) x thm =
+      let
+        fun zip_vars _ [] = []
+          | zip_vars (_ :: xs) (None :: opt_ts) = zip_vars xs opt_ts
+          | zip_vars ((x, _) :: xs) (Some t :: opt_ts) = (x, t) :: zip_vars xs opt_ts
+          | zip_vars [] _ = error "More instantiations than variables in theorem";
+        val insts =
+          zip_vars (Drule.vars_of_terms [#prop (Thm.rep_thm thm)]) args @
+          zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
+      in
+        thm
+        |> read_instantiate context_of insts x
+        |> RuleCases.save thm
+      end;
 
-val concl = Args.$$$ "concl" -- Args.$$$ ":";
+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 = Scan.lift (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x;
+fun insts' x = (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x;
 
-fun gen_of context_of = syntax (insts' >> (Drule.rule_attribute o read_instantiate' context_of));
+fun gen_of context_of =
+  syntax (Scan.lift insts' >> (Drule.rule_attribute o read_instantiate' context_of));
 
 val of_global = gen_of ProofContext.init;
 val of_local = gen_of I;