--- a/src/HOL/Integ/Bin.ML Wed Mar 22 12:45:41 2000 +0100
+++ b/src/HOL/Integ/Bin.ML Wed Mar 22 13:01:18 2000 +0100
@@ -213,8 +213,6 @@
(** Special simplification, for constants only **)
-fun inst x t = read_instantiate_sg (sign_of Bin.thy) [(x,t)];
-
(*Distributive laws for literals*)
Addsimps (map (inst "w" "number_of ?v")
[zadd_zmult_distrib, zadd_zmult_distrib2,
--- a/src/HOL/Integ/NatBin.ML Wed Mar 22 12:45:41 2000 +0100
+++ b/src/HOL/Integ/NatBin.ML Wed Mar 22 13:01:18 2000 +0100
@@ -285,8 +285,6 @@
qed "Suc_pred'";
-fun inst x t = read_instantiate_sg (sign_of NatBin.thy) [(x,t)];
-
(*Expresses a natural number constant as the Suc of another one.
NOT suitable for rewriting because n recurs in the condition.*)
bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
--- a/src/HOL/Real/RealBin.ML Wed Mar 22 12:45:41 2000 +0100
+++ b/src/HOL/Real/RealBin.ML Wed Mar 22 13:01:18 2000 +0100
@@ -141,9 +141,6 @@
fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
-fun inst x t = read_instantiate_sg (sign_of RealBin.thy) [(x,t)];
-
-
(*Now insert some identities previously stated for 0r and 1r*)
(** RealDef & Real **)