src/HOL/Tools/refute.ML

 						end
 						handle ERROR _         => get_typedefn axms
 						     | MATCH           => get_typedefn axms
 						     | Type.TYPE_MATCH => get_typedefn axms)
 				in
-					case DatatypePackage.datatype_info thy s of
+					case DatatypePackage.get_datatype thy s of
 					  SOME info =>  (* inductive datatype *)
 							(* only collect relevant type axioms for the argument types *)
 							Library.foldl collect_type_axioms (axs, Ts)
 					| NONE =>
 						(case get_typedefn axioms of

 					(* inductive data types *)
 					(* unit -> bool *)
 					fun is_IDT_constructor () =
 						(case body_type T of
 						  Type (s', _) =>
-							(case DatatypePackage.constrs_of thy s' of
+							(case DatatypePackage.get_datatype_constrs thy s' of
 							  SOME constrs =>
-								Library.exists (fn c =>
-									(case c of
-									  Const (cname, ctype) =>
-										cname = s andalso Sign.typ_instance thy (T, ctype)
-									| _ =>
-										raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
+								Library.exists (fn (cname, cty) =>
+								cname = s andalso Sign.typ_instance thy (T, cty))
 									constrs
 							| NONE =>
 								false)
 						| _  =>
 							false)

 				(case T of
 				  Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))
 				| Type ("prop", [])      => acc
 				| Type ("set", [T1])     => collect_types (T1, acc)
 				| Type (s, Ts)           =>
-					(case DatatypePackage.datatype_info thy s of
+					(case DatatypePackage.get_datatype thy s of
 					  SOME info =>  (* inductive datatype *)
 						let
 							val index               = #index info
 							val descr               = #descr info
 							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index

 			(* we can only consider fragments of recursive IDTs, so we issue a  *)
 			(* warning if the formula contains a recursive IDT                  *)
 			(* TODO: no warning needed for /positive/ occurrences of IDTs       *)
 			val _ = if Library.exists (fn
 				  Type (s, _) =>
-					(case DatatypePackage.datatype_info thy s of
+					(case DatatypePackage.get_datatype thy s of
 					  SOME info =>  (* inductive datatype *)
 						let
 							val index           = #index info
 							val descr           = #descr info
 							val (_, _, constrs) = (the o AList.lookup (op =) descr) index

 	fun IDT_interpreter thy model args t =
 	let
 		val (typs, terms) = model
 		(* Term.typ -> (interpretation * model * arguments) option *)
 		fun interpret_term (Type (s, Ts)) =
-			(case DatatypePackage.datatype_info thy s of
+			(case DatatypePackage.get_datatype thy s of
 			  SOME info =>  (* inductive datatype *)
 				let
 					(* int option -- only recursive IDTs have an associated depth *)
 					val depth = AList.lookup (op =) typs (Type (s, Ts))
 				in

 		| NONE =>
 			(case t of
 			  Const (s, T) =>
 				(case body_type T of
 				  Type (s', Ts') =>
-					(case DatatypePackage.datatype_info thy s' of
+					(case DatatypePackage.get_datatype thy s' of
 					  SOME info =>  (* body type is an inductive datatype *)
 						let
 							val index               = #index info
 							val descr               = #descr info
 							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index

 		  | typeof (Const (_, T)) = SOME T
 		  | typeof _              = NONE
 	in
 		case typeof t of
 		  SOME (Type (s, Ts)) =>
-			(case DatatypePackage.datatype_info thy s of
+			(case DatatypePackage.get_datatype thy s of
 			  SOME info =>  (* inductive datatype *)
 				let
 					val (typs, _)           = model
 					val index               = #index info
 					val descr               = #descr info