--- a/src/HOL/Tools/Function/inductive_wrap.ML Fri Oct 23 15:33:19 2009 +0200
+++ b/src/HOL/Tools/Function/inductive_wrap.ML Fri Oct 23 16:22:10 2009 +0200
@@ -6,17 +6,17 @@
the introduction and elimination rules.
*)
-signature FUNDEF_INDUCTIVE_WRAP =
+signature FUNCTION_INDUCTIVE_WRAP =
sig
val inductive_def : term list
-> ((bstring * typ) * mixfix) * local_theory
-> thm list * (term * thm * thm * local_theory)
end
-structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP =
+structure Function_Inductive_Wrap: FUNCTION_INDUCTIVE_WRAP =
struct
-open FundefLib
+open Function_Lib
fun requantify ctxt lfix orig_def thm =
let