src/Pure/Tools/rule_insts.ML

--- a/src/Pure/Tools/rule_insts.ML	Sat Jan 25 21:52:04 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sat Jan 25 22:06:07 2014 +0100
@@ -6,8 +6,8 @@
 
 signature BASIC_RULE_INSTS =
 sig
-  val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
-  val instantiate_tac: Proof.context -> (indexname * string) list -> tactic
+  val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
+  val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
   val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
   val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
   val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
@@ -20,6 +20,10 @@
 signature RULE_INSTS =
 sig
   include BASIC_RULE_INSTS
+  val where_rule: Proof.context -> (indexname * string) list ->
+    (binding * string option * mixfix) list -> thm -> thm
+  val of_rule: Proof.context -> string option list * string option list ->
+    (binding * string option * mixfix) list -> thm -> thm
   val make_elim_preserve: thm -> thm
   val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
     (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
@@ -123,9 +127,10 @@
     (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
   end;
 
-fun read_instantiate_mixed ctxt mixed_insts thm =
+fun where_rule ctxt mixed_insts fixes thm =
   let
     val ctxt' = ctxt
+      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
       |> Variable.declare_thm thm
       |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []);  (* FIXME !? *)
     val tvars = Thm.fold_terms Term.add_tvars thm [];
@@ -133,10 +138,11 @@
     val insts = read_insts ctxt' mixed_insts (tvars, vars);
   in
     Drule.instantiate_normalize insts thm
+    |> singleton (Proof_Context.export ctxt' ctxt)
     |> Rule_Cases.save thm
   end;
 
-fun read_instantiate_mixed' ctxt (args, concl_args) thm =
+fun of_rule ctxt (args, concl_args) fixes thm =
   let
     fun zip_vars _ [] = []
       | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
@@ -145,17 +151,18 @@
     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_mixed ctxt insts thm end;
+  in where_rule ctxt insts fixes thm end;
 
 end;
 
 
 (* instantiation of rule or goal state *)
 
-fun read_instantiate ctxt =
-  read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic);  (* FIXME !? *)
+fun read_instantiate ctxt insts xs =
+  where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
 
-fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
+fun instantiate_tac ctxt insts fixes =
+  PRIMITIVE (read_instantiate ctxt insts fixes);
 
 
 
@@ -165,9 +172,10 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding "where"}
-    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
-      (fn args =>
-        Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+    (Scan.lift
+      (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax)) -- Parse.for_fixes) >>
+      (fn (insts, fixes) =>
+        Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes)))
     "named instantiation of theorem");
 
 
@@ -186,8 +194,8 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding "of"}
-    (Scan.lift insts >> (fn args =>
-      Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+    (Scan.lift (insts -- Parse.for_fixes) >> (fn (args, fixes) =>
+      Thm.rule_attribute (fn context => of_rule (Context.proof_of context) args fixes)))
     "positional instantiation of theorem");
 
 end;