--- a/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 14:10:45 2008 +0200
@@ -14,7 +14,7 @@
-> thm list * (term * thm * thm * local_theory)
end
-structure FundefInductiveWrap =
+structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP =
struct
open FundefLib
@@ -44,14 +44,14 @@
{quiet_mode = false,
verbose = ! Toplevel.debug,
kind = Thm.internalK,
- alt_name = "",
+ alt_name = Name.no_binding,
coind = false,
no_elim = false,
no_ind = false,
skip_mono = true}
- [((R, T), NoSyn)] (* the relation *)
+ [((Name.binding R, T), NoSyn)] (* the relation *)
[] (* no parameters *)
- (map (fn t => (("", []), t)) defs) (* the intros *)
+ (map (fn t => ((Name.no_binding, []), t)) defs) (* the intros *)
[] (* no special monos *)
lthy