# HG changeset patch
# User wenzelm
# Date 1437941257 -7200
# Node ID e3f2262786ea78d4ca2af2b8a7961ffec8e71c5e
# Parent  2f39d95ac55dcd4fdfa864828041122906e0eae9
updated to infer_instantiate;

diff -r 2f39d95ac55d -r e3f2262786ea src/Doc/Eisbach/Base.thy
--- 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>
diff -r 2f39d95ac55d -r e3f2262786ea src/HOL/Eisbach/eisbach_rule_insts.ML
--- 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
diff -r 2f39d95ac55d -r e3f2262786ea src/HOL/Eisbach/match_method.ML
--- 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