# HG changeset patch
# User wenzelm
# Date 1213631690 -7200
# Node ID 80356567e7ad598e4cb0e6db791826d096c9edf0
# Parent  134991516430a9ae1e098121556b87ea19a88828
added read_instantiate;

diff -r 134991516430 -r 80356567e7ad src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Mon Jun 16 17:54:49 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Mon Jun 16 17:54:50 2008 +0200
@@ -7,6 +7,7 @@
 
 signature RULE_INSTS =
 sig
+  val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
   val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
     thm -> int -> tactic
   val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
@@ -143,7 +144,7 @@
       (map (pairself certT) inst_tvars, map (pairself cert) inst_vars))
   end;
 
-fun read_instantiate ctxt mixed_insts thm =
+fun read_instantiate_mixed ctxt mixed_insts thm =
   let
     val ctxt' = ctxt |> Variable.declare_thm thm
       |> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []);  (* FIXME tmp *)
@@ -161,7 +162,7 @@
     Drule.instantiate insts thm |> RuleCases.save thm
   end;
 
-fun read_instantiate' ctxt (args, concl_args) thm =
+fun read_instantiate_mixed' ctxt (args, concl_args) thm =
   let
     fun zip_vars _ [] = []
       | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
@@ -170,7 +171,11 @@
     val insts =
       zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
       zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
-  in read_instantiate ctxt insts thm end;
+  in read_instantiate_mixed ctxt insts thm end;
+
+fun read_instantiate ctxt args thm =
+  read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
+    (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm;
 
 end;
 
@@ -193,7 +198,7 @@
 in
 
 val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
-  Thm.rule_attribute (fn context => read_instantiate (Context.proof_of context) args)));
+  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
 
 end;
 
@@ -216,7 +221,7 @@
 in
 
 val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
-  Thm.rule_attribute (fn context => read_instantiate' (Context.proof_of context) args)));
+  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)));
 
 end;