author haftmann Fri, 13 Mar 2009 19:18:07 +0100 changeset 30520 c4728771f04f parent 30516 68b4a06cbd5c (current diff) parent 30519 c05c0199826f (diff) child 30521 3ec2d35b380f child 30531 ab3d61baf66a
merged
```--- a/src/HOL/IntDiv.thy	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/HOL/IntDiv.thy	Fri Mar 13 19:18:07 2009 +0100
@@ -512,15 +512,12 @@
(* simprocs adapted from HOL/ex/Binary.thy *)
ML {*
local
-  infix ==;
-  val op == = Logic.mk_equals;
-  fun plus m n = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} \$ m \$ n;
-  fun mult m n = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"} \$ m \$ n;
-
-  val binary_ss = HOL_basic_ss addsimps @{thms arithmetic_simps};
-  fun prove ctxt prop =
-    Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
-
+  val mk_number = HOLogic.mk_number HOLogic.intT;
+  fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} \$
+    (@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} \$ u \$ mk_number k) \$
+      mk_number l;
+  fun prove ctxt prop = Goal.prove ctxt [] [] prop
+    (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));
fun binary_proc proc ss ct =
(case Thm.term_of ct of
_ \$ t \$ u =>
@@ -529,16 +526,11 @@
| NONE => NONE)
| _ => NONE);
in
-
-fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
-  if n = 0 then NONE
-  else
-    let val (k, l) = Integer.div_mod m n;
-        fun mk_num x = HOLogic.mk_number HOLogic.intT x;
-    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))])
-    end);
-
-end;
+  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
+    if n = 0 then NONE
+    else let val (k, l) = Integer.div_mod m n;
+    in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);
+end
*}

simproc_setup binary_int_div ("number_of m div number_of n :: int") =```
```--- a/src/HOL/Tools/arith_data.ML	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/HOL/Tools/arith_data.ML	Fri Mar 13 19:18:07 2009 +0100
@@ -10,6 +10,8 @@
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
val simp_all_tac: thm list -> simpset -> tactic
+  val simplify_meta_eq: thm list -> simpset -> thm -> thm
+  val trans_tac: thm option -> tactic
val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
-> simproc
end;
@@ -33,6 +35,13 @@
let val ss0 = HOL_ss addsimps rules
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;

+fun simplify_meta_eq rules =
+  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
+
+fun trans_tac NONE  = all_tac
+  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
+
fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
Simplifier.simproc (the_context ()) name pats proc;
```
```--- a/src/HOL/Tools/int_arith.ML	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/HOL/Tools/int_arith.ML	Fri Mar 13 19:18:07 2009 +0100
@@ -29,41 +29,6 @@
(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];

-(** New term ordering so that AC-rewriting brings numerals to the front **)
-
-(*Order integers by absolute value and then by sign. The standard integer
-  ordering is not well-founded.*)
-fun num_ord (i,j) =
-  (case int_ord (abs i, abs j) of
-    EQUAL => int_ord (Int.sign i, Int.sign j)
-  | ord => ord);
-
-(*This resembles TermOrd.term_ord, but it puts binary numerals before other
-  non-atomic terms.*)
-local open Term
-in
-fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
-      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
-  | numterm_ord
-     (Const(@{const_name Int.number_of}, _) \$ v, Const(@{const_name Int.number_of}, _) \$ w) =
-     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
-  | numterm_ord (Const(@{const_name Int.number_of}, _) \$ _, _) = LESS
-  | numterm_ord (_, Const(@{const_name Int.number_of}, _) \$ _) = GREATER
-  | numterm_ord (t, u) =
-      (case int_ord (size_of_term t, size_of_term u) of
-        EQUAL =>
-          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
-            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
-          end
-      | ord => ord)
-and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
-end;
-
-fun numtermless tu = (numterm_ord tu = LESS);
-
-(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
-val num_ss = HOL_ss settermless numtermless;
-

(** Utilities **)

@@ -177,6 +142,41 @@
in (mk_frac (p, 1), mk_divide (t', one_of T)) end;

+(** New term ordering so that AC-rewriting brings numerals to the front **)
+
+(*Order integers by absolute value and then by sign. The standard integer
+  ordering is not well-founded.*)
+fun num_ord (i,j) =
+  (case int_ord (abs i, abs j) of
+    EQUAL => int_ord (Int.sign i, Int.sign j)
+  | ord => ord);
+
+(*This resembles TermOrd.term_ord, but it puts binary numerals before other
+  non-atomic terms.*)
+local open Term
+in
+fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
+      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
+  | numterm_ord
+     (Const(@{const_name Int.number_of}, _) \$ v, Const(@{const_name Int.number_of}, _) \$ w) =
+     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
+  | numterm_ord (Const(@{const_name Int.number_of}, _) \$ _, _) = LESS
+  | numterm_ord (_, Const(@{const_name Int.number_of}, _) \$ _) = GREATER
+  | numterm_ord (t, u) =
+      (case int_ord (size_of_term t, size_of_term u) of
+        EQUAL =>
+          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
+            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
+          end
+      | ord => ord)
+and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
+end;
+
+fun numtermless tu = (numterm_ord tu = LESS);
+
+val num_ss = HOL_ss settermless numtermless;
+
+
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
@@ -218,14 +218,6 @@
val mult_minus_simps =
[@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];

-(*Apply the given rewrite (if present) just once*)
-fun trans_tac NONE      = all_tac
-  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
-
-fun simplify_meta_eq rules =
-  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
-
structure CancelNumeralsCommon =
struct
val mk_sum            = mk_sum
@@ -233,7 +225,7 @@
val mk_coeff          = mk_coeff
val dest_coeff        = dest_coeff 1
val find_first_coeff  = find_first_coeff []
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac

diff_simps @ minus_simps @ @{thms add_ac}
@@ -246,7 +238,7 @@

fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
-  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
end;

@@ -316,7 +308,7 @@
val dest_coeff        = dest_coeff 1
val left_distrib      = @{thm combine_common_factor} RS trans
val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac

diff_simps @ minus_simps @ @{thms add_ac}
@@ -329,7 +321,7 @@

fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
-  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
end;

structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
@@ -346,7 +338,7 @@
val dest_coeff        = dest_fcoeff 1
val left_distrib      = @{thm combine_common_factor} RS trans
val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac

inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
@@ -359,7 +351,7 @@

fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
-  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
end;

structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);```
```--- a/src/HOL/Tools/int_factor_simprocs.ML	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Fri Mar 13 19:18:07 2009 +0100
@@ -29,7 +29,7 @@
struct
val mk_coeff          = mk_coeff
val dest_coeff        = dest_coeff 1
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac

val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -41,7 +41,7 @@

val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
-  val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq
@{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
end
@@ -215,7 +215,7 @@
handle TERM _ => find_first_t (t::past) u terms;

(** Final simplification for the CancelFactor simprocs **)
-val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
+val simplify_one = Arith_Data.simplify_meta_eq
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];

fun cancel_simplify_meta_eq cancel_th ss th =
@@ -228,7 +228,7 @@
val mk_coeff          = mk_coeff
val dest_coeff        = dest_coeff
val find_first        = find_first_t []
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
end;```
```--- a/src/HOL/Tools/nat_simprocs.ML	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/HOL/Tools/nat_simprocs.ML	Fri Mar 13 19:18:07 2009 +0100
@@ -41,8 +41,6 @@

(** Other simproc items **)

-val trans_tac = Int_Numeral_Simprocs.trans_tac;
-
val bin_simps =
[@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
@@ -130,15 +128,11 @@
@{thm Suc_not_Zero}, @{thm le_0_eq}];

val simplify_meta_eq =
-    Int_Numeral_Simprocs.simplify_meta_eq
+    Arith_Data.simplify_meta_eq
@{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);

-(*Like HOL_ss but with an ordering that brings numerals to the front
-  under AC-rewriting.*)
-val num_ss = Int_Numeral_Simprocs.num_ss;
-
(*** Applying CancelNumeralsFun ***)

structure CancelNumeralsCommon =
@@ -148,11 +142,11 @@
val mk_coeff          = mk_coeff
val dest_coeff        = dest_coeff
val find_first_coeff  = find_first_coeff []
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac

-  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
+  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -237,10 +231,10 @@
val dest_coeff        = dest_coeff
val left_distrib      = @{thm left_add_mult_distrib} RS trans
val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac

-  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
+  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -262,11 +256,11 @@
struct
val mk_coeff          = mk_coeff
val dest_coeff        = dest_coeff
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac

-  val norm_ss1 = num_ss addsimps
+  val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps
-  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
+  val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -355,7 +349,7 @@
handle TERM _ => find_first_t (t::past) u terms;

(** Final simplification for the CancelFactor simprocs **)
-val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
+val simplify_one = Arith_Data.simplify_meta_eq
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];

fun cancel_simplify_meta_eq cancel_th ss th =
@@ -368,7 +362,7 @@
val mk_coeff          = mk_coeff
val dest_coeff        = dest_coeff
val find_first        = find_first_t []
-  val trans_tac         = fn _ => trans_tac
+  val trans_tac         = K Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
end;```
```--- a/src/Pure/Isar/class_target.ML	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 19:18:07 2009 +0100
@@ -43,8 +43,8 @@
val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
-> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
val conclude_instantiation: local_theory -> local_theory
-  val instantiation_param: local_theory -> string -> string option
-  val confirm_declaration: string -> local_theory -> local_theory
+  val instantiation_param: local_theory -> binding -> string option
+  val confirm_declaration: binding -> local_theory -> local_theory
val pretty_instantiation: local_theory -> Pretty.T
val type_name: string -> string

@@ -430,8 +430,8 @@

val instantiation_params = #params o get_instantiation;

-fun instantiation_param lthy v = instantiation_params lthy
-  |> find_first (fn (_, (v', _)) => v = v')
+fun instantiation_param lthy b = instantiation_params lthy
+  |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
|> Option.map (fst o fst);

@@ -530,8 +530,8 @@
|> synchronize_inst_syntax
end;

-fun confirm_declaration c = (map_instantiation o apsnd)
-  (filter_out (fn (_, (c', _)) => c' = c))
+fun confirm_declaration b = (map_instantiation o apsnd)
+  (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
#> LocalTheory.target synchronize_inst_syntax

fun gen_instantiation_instance do_proof after_qed lthy =```
```--- a/src/Pure/Isar/overloading.ML	Fri Mar 13 10:14:47 2009 -0700
@@ -9,9 +9,9 @@
val init: (string * (string * typ) * bool) list -> theory -> local_theory
val conclude: local_theory -> local_theory
val declare: string * typ -> theory -> term * theory
-  val confirm: string -> local_theory -> local_theory
-  val define: bool -> string -> string * term -> theory -> thm * theory
-  val operation: Proof.context -> string -> (string * bool) option
+  val confirm: binding -> local_theory -> local_theory
+  val define: bool -> binding -> string * term -> theory -> thm * theory
+  val operation: Proof.context -> binding -> (string * bool) option
val pretty: Proof.context -> Pretty.T

type improvable_syntax
@@ -123,18 +123,19 @@

-  |> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
+  |> get_first (fn ((c, _), (v, checked)) =>
+      if Binding.name_of b = v then SOME (c, checked) else NONE);

-fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
+fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));

(* overloaded declarations and definitions *)

fun declare c_ty = pair (Const c_ty);

-fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
-  Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked b (c, t) = Thm.add_def (not checked) true
+  (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));

(* target *)```
```--- a/src/Pure/Isar/theory_target.ML	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/Pure/Isar/theory_target.ML	Fri Mar 13 19:18:07 2009 +0100
@@ -188,10 +188,7 @@
in
not (is_class andalso (similar_body orelse class_global)) ?
(Context.mapping_result
-        (fn thy => thy
-          |> Sign.no_base_names
-          |> Sign.add_abbrev PrintMode.internal tags legacy_arg
-          ||> Sign.restore_naming thy)
#-> (fn (lhs' as Const (d, _), _) =>
similar_body ?
@@ -203,23 +200,22 @@

fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
let
-    val c = Binding.qualified_name_of b;
val tags = LocalTheory.group_position_of lthy;
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
val U = map #2 xs ---> T;
val (mx1, mx2, mx3) = fork_mixfix ta mx;
val declare_const =
-      (case Class_Target.instantiation_param lthy c of
+      (case Class_Target.instantiation_param lthy b of
SOME c' =>
if mx3 <> NoSyn then syntax_error c'
-            ##> Class_Target.confirm_declaration c
+            ##> Class_Target.confirm_declaration b
| NONE =>
SOME (c', _) =>
if mx3 <> NoSyn then syntax_error c'
| NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
val (const, lthy') = lthy |> declare_const;
val t = Term.list_comb (const, map Free xs);
@@ -282,17 +278,14 @@
val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);

(*def*)
-    val c = Binding.qualified_name_of b;
-    val define_const =
-        SOME (_, checked) =>
-          (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
-      | NONE =>
-          if is_none (Class_Target.instantiation_param lthy c)
-          then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
-          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
val (global_def, lthy3) = lthy2
-      |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
+          SOME (_, checked) =>
+        | NONE =>
+            if is_none (Class_Target.instantiation_param lthy b)
+            then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
+            else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
val def = LocalDefs.trans_terms lthy3
[(*c == global.c xs*)     local_def,
(*global.c xs == rhs'*)  global_def,```
```--- a/src/Pure/axclass.ML	Fri Mar 13 10:14:47 2009 -0700
+++ b/src/Pure/axclass.ML	Fri Mar 13 19:18:07 2009 +0100
@@ -27,7 +27,7 @@
val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
val instance_name: string * class -> string
val declare_overloaded: string * typ -> theory -> term * theory
-  val define_overloaded: string -> string * term -> theory -> thm * theory
+  val define_overloaded: binding -> string * term -> theory -> thm * theory
val inst_tyco_of: theory -> string * typ -> string option
val unoverload: theory -> thm -> thm
val overload: theory -> thm -> thm
@@ -383,16 +383,17 @@
#> pair (Const (c, T))))
end;

-fun define_overloaded name (c, t) thy =
+fun define_overloaded b (c, t) thy =
let
val T = Term.fastype_of t;
val SOME tyco = inst_tyco_of thy (c, T);
val (c', eq) = get_inst_param thy (c, tyco);
val prop = Logic.mk_equals (Const (c', T), t);
-    val name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name;
+    val b' = Thm.def_binding_optional
+      (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b;
in
thy
-    |> Thm.add_def false false (Binding.name name', prop)
+    |> Thm.add_def false false (b', prop)
|>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
end;
```