src/HOL/Tools/refute.ML
changeset 19346 c4c003abd830
parent 19277 f7602e74d948
child 19642 ea7162f84677
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Apr 06 16:10:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Apr 06 16:10:46 2006 +0200
     1.3 @@ -554,7 +554,7 @@
     1.4  						     | MATCH           => get_typedefn axms
     1.5  						     | Type.TYPE_MATCH => get_typedefn axms)
     1.6  				in
     1.7 -					case DatatypePackage.datatype_info thy s of
     1.8 +					case DatatypePackage.get_datatype thy s of
     1.9  					  SOME info =>  (* inductive datatype *)
    1.10  							(* only collect relevant type axioms for the argument types *)
    1.11  							Library.foldl collect_type_axioms (axs, Ts)
    1.12 @@ -664,14 +664,10 @@
    1.13  					fun is_IDT_constructor () =
    1.14  						(case body_type T of
    1.15  						  Type (s', _) =>
    1.16 -							(case DatatypePackage.constrs_of thy s' of
    1.17 +							(case DatatypePackage.get_datatype_constrs thy s' of
    1.18  							  SOME constrs =>
    1.19 -								Library.exists (fn c =>
    1.20 -									(case c of
    1.21 -									  Const (cname, ctype) =>
    1.22 -										cname = s andalso Sign.typ_instance thy (T, ctype)
    1.23 -									| _ =>
    1.24 -										raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
    1.25 +								Library.exists (fn (cname, cty) =>
    1.26 +								cname = s andalso Sign.typ_instance thy (T, cty))
    1.27  									constrs
    1.28  							| NONE =>
    1.29  								false)
    1.30 @@ -773,7 +769,7 @@
    1.31  				| Type ("prop", [])      => acc
    1.32  				| Type ("set", [T1])     => collect_types (T1, acc)
    1.33  				| Type (s, Ts)           =>
    1.34 -					(case DatatypePackage.datatype_info thy s of
    1.35 +					(case DatatypePackage.get_datatype thy s of
    1.36  					  SOME info =>  (* inductive datatype *)
    1.37  						let
    1.38  							val index               = #index info
    1.39 @@ -944,7 +940,7 @@
    1.40  			(* TODO: no warning needed for /positive/ occurrences of IDTs       *)
    1.41  			val _ = if Library.exists (fn
    1.42  				  Type (s, _) =>
    1.43 -					(case DatatypePackage.datatype_info thy s of
    1.44 +					(case DatatypePackage.get_datatype thy s of
    1.45  					  SOME info =>  (* inductive datatype *)
    1.46  						let
    1.47  							val index           = #index info
    1.48 @@ -1647,7 +1643,7 @@
    1.49  		val (typs, terms) = model
    1.50  		(* Term.typ -> (interpretation * model * arguments) option *)
    1.51  		fun interpret_term (Type (s, Ts)) =
    1.52 -			(case DatatypePackage.datatype_info thy s of
    1.53 +			(case DatatypePackage.get_datatype thy s of
    1.54  			  SOME info =>  (* inductive datatype *)
    1.55  				let
    1.56  					(* int option -- only recursive IDTs have an associated depth *)
    1.57 @@ -1723,7 +1719,7 @@
    1.58  			  Const (s, T) =>
    1.59  				(case body_type T of
    1.60  				  Type (s', Ts') =>
    1.61 -					(case DatatypePackage.datatype_info thy s' of
    1.62 +					(case DatatypePackage.get_datatype thy s' of
    1.63  					  SOME info =>  (* body type is an inductive datatype *)
    1.64  						let
    1.65  							val index               = #index info
    1.66 @@ -2511,7 +2507,7 @@
    1.67  	in
    1.68  		case typeof t of
    1.69  		  SOME (Type (s, Ts)) =>
    1.70 -			(case DatatypePackage.datatype_info thy s of
    1.71 +			(case DatatypePackage.get_datatype thy s of
    1.72  			  SOME info =>  (* inductive datatype *)
    1.73  				let
    1.74  					val (typs, _)           = model