# HG changeset patch
# User wenzelm
# Date 1441887142 -7200
# Node ID d85d8f5e921b57b8510c462b6e596d98c32c91b8
# Parent  3e28b08d62c0d0e729e25486ee6f76f156eb7b21
tuned -- avoid slightly odd @{cpat};

diff -r 3e28b08d62c0 -r d85d8f5e921b src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Thu Sep 10 11:59:12 2015 +0200
+++ b/src/HOL/Tools/numeral.ML	Thu Sep 10 14:12:22 2015 +0200
@@ -37,27 +37,33 @@
 
 local
 
-val zero = @{cpat "0"};
-val zeroT = Thm.ctyp_of_cterm zero;
+val cterm_of = Thm.cterm_of @{context};
+fun tvar S = (("'a", 0), S);
 
-val one = @{cpat "1"};
-val oneT = Thm.ctyp_of_cterm one;
+val zero_tvar = tvar @{sort zero};
+val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar));
 
-val numeral = @{cpat "numeral"};
-val numeralT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm numeral));
+val one_tvar = tvar @{sort one};
+val one = cterm_of (Const (@{const_name one_class.one}, TVar one_tvar));
 
-val uminus = @{cpat "uminus"};
-val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus));
+val numeral_tvar = tvar @{sort numeral};
+val numeral = cterm_of (Const (@{const_name numeral}, @{typ num} --> TVar numeral_tvar));
 
-fun instT T V = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of V), T)], []);
+val uminus_tvar = tvar @{sort uminus};
+val uminus = cterm_of (Const (@{const_name uminus}, TVar uminus_tvar --> TVar uminus_tvar));
+
+fun instT T v = Thm.instantiate_cterm ([(v, T)], []);
 
 in
 
-fun mk_cnumber T 0 = instT T zeroT zero
-  | mk_cnumber T 1 = instT T oneT one
+fun mk_cnumber T 0 = instT T zero_tvar zero
+  | mk_cnumber T 1 = instT T one_tvar one
   | mk_cnumber T i =
-    if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
-    else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i)));
+      if i > 0 then
+        Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral i)
+      else
+        Thm.apply (instT T uminus_tvar uminus)
+          (Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral (~ i)));
 
 end;
 
diff -r 3e28b08d62c0 -r d85d8f5e921b src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Sep 10 11:59:12 2015 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Sep 10 14:12:22 2015 +0200
@@ -584,23 +584,28 @@
 
 local
 
-val zr = @{cpat "0"}
-val zT = Thm.ctyp_of_cterm zr
-val geq = @{cpat HOL.eq}
-val eqT = Thm.dest_ctyp (Thm.ctyp_of_cterm geq) |> hd
+val cterm_of = Thm.cterm_of @{context};
+fun tvar S = (("'a", 0), S);
+
+val zero_tvar = tvar @{sort zero};
+val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar));
+
+val type_tvar = tvar @{sort type};
+val geq = cterm_of (Const (@{const_name HOL.eq}, TVar type_tvar --> TVar type_tvar --> @{typ bool}));
+
 val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
 val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
 val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
 
 fun prove_nz ctxt T t =
   let
-    val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr
-    val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq
-    val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
-         (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
-                (Thm.apply (Thm.apply eq t) z)))
-  in Thm.equal_elim (Thm.symmetric th) TrueI
-  end
+    val z = Thm.instantiate_cterm ([(zero_tvar, T)], []) zero
+    val eq = Thm.instantiate_cterm ([(type_tvar, T)], []) geq
+    val th =
+      Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
+        (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
+          (Thm.apply (Thm.apply eq t) z)))
+  in Thm.equal_elim (Thm.symmetric th) TrueI end
 
 fun proc ctxt ct =
   let