--- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Sun Jul 05 15:02:30 2015 +0200
@@ -258,8 +258,9 @@
local
val pth_zero = @{thm norm_zero}
- val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
- pth_zero
+ val tv_n =
+ (dest_TVar o Thm.typ_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
+ pth_zero
val concl = Thm.dest_arg o Thm.cprop_of
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
let
@@ -356,7 +357,7 @@
val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (#hyps (Thm.crep_thm th1))
val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
val cps = map (swap o Thm.dest_equals) (cprems_of th11)
- val th12 = Drule.instantiate_normalize ([], cps) th11
+ val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11
val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
in hd (Variable.export ctxt' ctxt [th13])
end