# HG changeset patch
# User paulson
# Date 953726478 -3600
# Node ID 8c4ff19a7286a611a12330ca5b078b8ff7be3ddf
# Parent  5c22595bc599f1b50250b478f74f9b3a670bb26a
tidied using new "inst" rule

diff -r 5c22595bc599 -r 8c4ff19a7286 src/HOL/Integ/Bin.ML
--- 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,
diff -r 5c22595bc599 -r 8c4ff19a7286 src/HOL/Integ/NatBin.ML
--- 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');
diff -r 5c22595bc599 -r 8c4ff19a7286 src/HOL/Real/RealBin.ML
--- 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 **)