--- a/src/Doc/Eisbach/Base.thy Sun Jul 26 21:50:44 2015 +0200
+++ b/src/Doc/Eisbach/Base.thy Sun Jul 26 22:07:37 2015 +0200
@@ -28,10 +28,10 @@
val datatype_var =
(case find_first (fn (_, T') => is_datatype T') vars of
- SOME var => Thm.cterm_of ctxt (Term.Var var)
+ SOME (xi, _) => xi
| NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
in
- SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
+ SOME (infer_instantiate ctxt [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
end
handle TERM _ => NONE;
\<close>
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jul 26 21:50:44 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jul 26 22:07:37 2015 +0200
@@ -6,7 +6,7 @@
Alternate syntax for rule_insts.ML participates in token closures by
examining the behaviour of Rule_Insts.where_rule and instantiating token
values accordingly. Instantiations in re-interpretation are done with
-Drule.cterm_instantiate.
+infer_instantiate.
*)
structure Eisbach_Rule_Insts: sig end =
@@ -57,13 +57,13 @@
SOME S => (((xi, S), Thm.ctyp_of ctxt (Logic.dest_type t)) :: Ts, ts)
| NONE =>
(case AList.lookup (op =) tvars xi of
- SOME T => (Ts, (Thm.cterm_of ctxt (Var (xi, T)), Thm.cterm_of ctxt t) :: ts)
+ SOME _ => (Ts, (xi, Thm.cterm_of ctxt t) :: ts)
| NONE => error "indexname not found in thm"));
- val (cTinsts, cinsts) = fold add_inst insts ([], []);
+ val (instT, inst) = fold add_inst insts ([], []);
in
- (Thm.instantiate (cTinsts, []) thm
- |> Drule.cterm_instantiate cinsts
+ (Thm.instantiate (instT, []) thm
+ |> infer_instantiate ctxt inst
COMP_INCR asm_rl)
|> Thm.adjust_maxidx_thm ~1
|> restore_tags thm
--- a/src/HOL/Eisbach/match_method.ML Sun Jul 26 21:50:44 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Sun Jul 26 22:07:37 2015 +0200
@@ -259,10 +259,8 @@
fun inst_thm ctxt env ts params thm =
let
val ts' = map (Envir.norm_term env) ts;
- val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params;
- in
- Drule.cterm_instantiate insts thm
- end;
+ val insts = map (#1 o dest_Var) ts' ~~ map (Thm.cterm_of ctxt) params;
+ in infer_instantiate ctxt insts thm end;
fun do_inst fact_insts' env text ctxt =
let