src/Tools/IsaPlanner/rw_inst.ML

--- a/src/Tools/IsaPlanner/rw_inst.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -174,7 +174,7 @@
     val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
 
     (* certified instantiations for types *)
-    val ctyp_insts = map (fn (ix, (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (ix, s), ty)) typinsts;
+    val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts;
 
     (* type instantiated versions *)
     val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
@@ -198,7 +198,7 @@
 
     (* create certms of instantiations *)
     val cinsts_tyinst =
-      map (fn (ix, (ty, t)) => apply2 (Thm.cterm_of ctxt) (Var (ix, ty), t)) insts_tyinst_inst;
+      map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst;
 
     (* The instantiated rule *)
     val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
@@ -217,7 +217,7 @@
     val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst);
     val (cprems, abstract_rule_inst) =
       rule_inst
-      |> Thm.instantiate ([], cterm_renamings)
+      |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings)
       |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
     val specific_tgt_rule =
       Conv.fconv_rule Drule.beta_eta_conversion
@@ -227,7 +227,7 @@
     val tgt_th_inst =
       tgt_th_tyinst
       |> Thm.instantiate ([], cinsts_tyinst)
-      |> Thm.instantiate ([], cterm_renamings);
+      |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings);
 
     val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   in