1.1 --- a/src/HOL/Integ/Bin.ML	Wed Mar 22 12:45:41 2000 +0100
     1.2 +++ b/src/HOL/Integ/Bin.ML	Wed Mar 22 13:01:18 2000 +0100
     1.3 @@ -213,8 +213,6 @@
     1.4  
     1.5  (** Special simplification, for constants only **)
     1.6  
     1.7 -fun inst x t = read_instantiate_sg (sign_of Bin.thy) [(x,t)];
     1.8 -
     1.9  (*Distributive laws for literals*)
    1.10  Addsimps (map (inst "w" "number_of ?v")
    1.11  	  [zadd_zmult_distrib, zadd_zmult_distrib2,

     2.1 --- a/src/HOL/Integ/NatBin.ML	Wed Mar 22 12:45:41 2000 +0100
     2.2 +++ b/src/HOL/Integ/NatBin.ML	Wed Mar 22 13:01:18 2000 +0100
     2.3 @@ -285,8 +285,6 @@
     2.4  qed "Suc_pred'";
     2.5  
     2.6  
     2.7 -fun inst x t = read_instantiate_sg (sign_of NatBin.thy) [(x,t)];
     2.8 -
     2.9  (*Expresses a natural number constant as the Suc of another one.
    2.10    NOT suitable for rewriting because n recurs in the condition.*)
    2.11  bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');

     3.1 --- a/src/HOL/Real/RealBin.ML	Wed Mar 22 12:45:41 2000 +0100
     3.2 +++ b/src/HOL/Real/RealBin.ML	Wed Mar 22 13:01:18 2000 +0100
     3.3 @@ -141,9 +141,6 @@
     3.4  fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
     3.5  
     3.6  
     3.7 -fun inst x t = read_instantiate_sg (sign_of RealBin.thy) [(x,t)];
     3.8 -
     3.9 -
    3.10  (*Now insert some identities previously stated for 0r and 1r*)
    3.11  
    3.12  (** RealDef & Real **)