added read_instantiate;
authorwenzelm
Mon Jun 16 17:54:50 2008 +0200 (2008-06-16)
changeset 2723680356567e7ad
parent 27235 134991516430
child 27237 c94eefffc3a5
added read_instantiate;
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Jun 16 17:54:49 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Jun 16 17:54:50 2008 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature RULE_INSTS =
     1.6  sig
     1.7 +  val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
     1.8    val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
     1.9      thm -> int -> tactic
    1.10    val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    1.11 @@ -143,7 +144,7 @@
    1.12        (map (pairself certT) inst_tvars, map (pairself cert) inst_vars))
    1.13    end;
    1.14  
    1.15 -fun read_instantiate ctxt mixed_insts thm =
    1.16 +fun read_instantiate_mixed ctxt mixed_insts thm =
    1.17    let
    1.18      val ctxt' = ctxt |> Variable.declare_thm thm
    1.19        |> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []);  (* FIXME tmp *)
    1.20 @@ -161,7 +162,7 @@
    1.21      Drule.instantiate insts thm |> RuleCases.save thm
    1.22    end;
    1.23  
    1.24 -fun read_instantiate' ctxt (args, concl_args) thm =
    1.25 +fun read_instantiate_mixed' ctxt (args, concl_args) thm =
    1.26    let
    1.27      fun zip_vars _ [] = []
    1.28        | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
    1.29 @@ -170,7 +171,11 @@
    1.30      val insts =
    1.31        zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
    1.32        zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
    1.33 -  in read_instantiate ctxt insts thm end;
    1.34 +  in read_instantiate_mixed ctxt insts thm end;
    1.35 +
    1.36 +fun read_instantiate ctxt args thm =
    1.37 +  read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
    1.38 +    (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm;
    1.39  
    1.40  end;
    1.41  
    1.42 @@ -193,7 +198,7 @@
    1.43  in
    1.44  
    1.45  val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
    1.46 -  Thm.rule_attribute (fn context => read_instantiate (Context.proof_of context) args)));
    1.47 +  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
    1.48  
    1.49  end;
    1.50  
    1.51 @@ -216,7 +221,7 @@
    1.52  in
    1.53  
    1.54  val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
    1.55 -  Thm.rule_attribute (fn context => read_instantiate' (Context.proof_of context) args)));
    1.56 +  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)));
    1.57  
    1.58  end;
    1.59