src/HOL/Tools/refute.ML
changeset 15570 8d8c70b41bab
parent 15547 f08e2d83681e
child 15571 c166086feace
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4  	fun tree_foldl f =
     1.5  	let
     1.6  		fun itl (e, Leaf x)  = f(e,x)
     1.7 -		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
     1.8 +		  | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs)
     1.9  	in
    1.10  		itl
    1.11  	end;
    1.12 @@ -192,7 +192,7 @@
    1.13  			 parameters = Symtab.merge (op=) (pa1, pa2)};
    1.14  		fun print sg {interpreters, printers, parameters} =
    1.15  			Pretty.writeln (Pretty.chunks
    1.16 -				[Pretty.strs ("default parameters:" :: flat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
    1.17 +				[Pretty.strs ("default parameters:" :: List.concat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
    1.18  				 Pretty.strs ("interpreters:" :: map fst interpreters),
    1.19  				 Pretty.strs ("printers:" :: map fst printers)]);
    1.20  	end;
    1.21 @@ -250,7 +250,7 @@
    1.22  			if null terms then
    1.23  				"empty interpretation (no free variables in term)\n"
    1.24  			else
    1.25 -				space_implode "\n" (mapfilter (fn (t,intr) =>
    1.26 +				space_implode "\n" (List.mapPartial (fn (t,intr) =>
    1.27  					(* print constants only if 'show_consts' is true *)
    1.28  					if (!show_consts) orelse not (is_Const t) then
    1.29  						SOME (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment))
    1.30 @@ -359,9 +359,9 @@
    1.31  		(* TODO: it is currently not possible to specify a size for a type     *)
    1.32  		(*       whose name is one of the other parameters (e.g. 'maxvars')    *)
    1.33  		(* (string * int) list *)
    1.34 -		val sizes     = mapfilter
    1.35 +		val sizes     = List.mapPartial
    1.36  			(fn (name,value) => (case Int.fromString value of SOME i => SOME (name, i) | NONE => NONE))
    1.37 -			(filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver")
    1.38 +			(List.filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver")
    1.39  				allparams)
    1.40  	in
    1.41  		{sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, maxtime=maxtime, satsolver=satsolver}
    1.42 @@ -382,12 +382,12 @@
    1.43  
    1.44  	fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    1.45  		(* replace a 'DtTFree' variable by the associated type *)
    1.46 -		(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
    1.47 +		(valOf o assoc) (typ_assoc, DatatypeAux.DtTFree a)
    1.48  	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    1.49  		Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.50  	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.51  		let
    1.52 -			val (s, ds, _) = (the o assoc) (descr, i)
    1.53 +			val (s, ds, _) = (valOf o assoc) (descr, i)
    1.54  		in
    1.55  			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.56  		end;
    1.57 @@ -419,7 +419,7 @@
    1.58  	let
    1.59  		val _ = immediate_output "Adding axioms..."
    1.60  		(* (string * Term.term) list *)
    1.61 -		val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
    1.62 +		val axioms = List.concat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
    1.63  		(* string list *)
    1.64  		val rec_names = Symtab.foldl (fn (acc, (_, info)) =>
    1.65  			#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)
    1.66 @@ -478,7 +478,7 @@
    1.67  					let
    1.68  						(* obtain the axioms generated by the "axclass" command *)
    1.69  						(* (string * Term.term) list *)
    1.70 -						val class_axioms             = filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms
    1.71 +						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms
    1.72  						(* replace the one schematic type variable in each axiom by the actual type 'T' *)
    1.73  						(* (string * Term.term) list *)
    1.74  						val monomorphic_class_axioms = map (fn (axname, ax) =>
    1.75 @@ -498,7 +498,7 @@
    1.76  								collect_term_axioms (ax :: axs, ax)
    1.77  							)
    1.78  					in
    1.79 -						foldl collect_axiom (axs, monomorphic_class_axioms)
    1.80 +						Library.foldl collect_axiom (axs, monomorphic_class_axioms)
    1.81  					end
    1.82  				(* string list *)
    1.83  				val sort = (case T of
    1.84 @@ -509,7 +509,7 @@
    1.85  				(* string list *)
    1.86  				val superclasses = Graph.all_succs ((#classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
    1.87  			in
    1.88 -				foldl collect_class_axioms (axs, superclasses)
    1.89 +				Library.foldl collect_class_axioms (axs, superclasses)
    1.90  			end
    1.91  		(* Term.term list * Term.typ -> Term.term list *)
    1.92  		and collect_type_axioms (axs, T) =
    1.93 @@ -557,20 +557,20 @@
    1.94  					case DatatypePackage.datatype_info thy s of
    1.95  					  SOME info =>  (* inductive datatype *)
    1.96  							(* only collect relevant type axioms for the argument types *)
    1.97 -							foldl collect_type_axioms (axs, Ts)
    1.98 +							Library.foldl collect_type_axioms (axs, Ts)
    1.99  					| NONE =>
   1.100  						(case get_typedefn axioms of
   1.101  						  SOME (axname, ax) => 
   1.102  							if mem_term (ax, axs) then
   1.103  								(* only collect relevant type axioms for the argument types *)
   1.104 -								foldl collect_type_axioms (axs, Ts)
   1.105 +								Library.foldl collect_type_axioms (axs, Ts)
   1.106  							else
   1.107  								(immediate_output (" " ^ axname);
   1.108  								collect_term_axioms (ax :: axs, ax))
   1.109  						| NONE =>
   1.110  							(* unspecified type, perhaps introduced with 'typedecl' *)
   1.111  							(* at least collect relevant type axioms for the argument types *)
   1.112 -							foldl collect_type_axioms (axs, Ts))
   1.113 +							Library.foldl collect_type_axioms (axs, Ts))
   1.114  				end
   1.115  			| TFree _                => collect_sort_axioms (axs, T)  (* axiomatic type classes *)
   1.116  			| TVar _                 => collect_sort_axioms (axs, T)  (* axiomatic type classes *)
   1.117 @@ -590,7 +590,7 @@
   1.118  			| Const ("arbitrary", T)          => collect_type_axioms (axs, T)
   1.119  			| Const ("The", T)                =>
   1.120  				let
   1.121 -					val ax = specialize_type (("The", T), (the o assoc) (axioms, "HOL.the_eq_trivial"))
   1.122 +					val ax = specialize_type (("The", T), (valOf o assoc) (axioms, "HOL.the_eq_trivial"))
   1.123  				in
   1.124  					if mem_term (ax, axs) then
   1.125  						collect_type_axioms (axs, T)
   1.126 @@ -600,7 +600,7 @@
   1.127  				end
   1.128  			| Const ("Hilbert_Choice.Eps", T) =>
   1.129  				let
   1.130 -					val ax = specialize_type (("Hilbert_Choice.Eps", T), (the o assoc) (axioms, "Hilbert_Choice.someI"))
   1.131 +					val ax = specialize_type (("Hilbert_Choice.Eps", T), (valOf o assoc) (axioms, "Hilbert_Choice.someI"))
   1.132  				in
   1.133  					if mem_term (ax, axs) then
   1.134  						collect_type_axioms (axs, T)
   1.135 @@ -686,7 +686,7 @@
   1.136  							val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
   1.137  							(* Term.term option *)
   1.138  							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
   1.139 -							val intro_ax   = (apsome (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
   1.140 +							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
   1.141  							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
   1.142  									(* collect relevant type axioms *)
   1.143  									collect_type_axioms (axs, T)
   1.144 @@ -734,7 +734,7 @@
   1.145  			(* (Term.indexname * Term.typ) list *)
   1.146  			val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   1.147  		in
   1.148 -			foldl
   1.149 +			Library.foldl
   1.150  				(fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x, i), T), t')))
   1.151  				(t, vars)
   1.152  		end
   1.153 @@ -772,7 +772,7 @@
   1.154  						let
   1.155  							val index               = #index info
   1.156  							val descr               = #descr info
   1.157 -							val (_, dtyps, constrs) = (the o assoc) (descr, index)
   1.158 +							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.159  							val typ_assoc           = dtyps ~~ Ts
   1.160  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.161  							val _ = (if Library.exists (fn d =>
   1.162 @@ -787,14 +787,14 @@
   1.163  								else
   1.164  									acc)
   1.165  							(* collect argument types *)
   1.166 -							val acc_args = foldr collect_types (Ts, acc')
   1.167 +							val acc_args = Library.foldr collect_types (Ts, acc')
   1.168  							(* collect constructor types *)
   1.169 -							val acc_constrs = foldr collect_types (flat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
   1.170 +							val acc_constrs = Library.foldr collect_types (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
   1.171  						in
   1.172  							acc_constrs
   1.173  						end
   1.174  					| NONE =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
   1.175 -						T ins (foldr collect_types (Ts, acc)))
   1.176 +						T ins (Library.foldr collect_types (Ts, acc)))
   1.177  				| TFree _                => T ins acc
   1.178  				| TVar _                 => T ins acc)
   1.179  	in
   1.180 @@ -853,9 +853,9 @@
   1.181  				NONE
   1.182  		  | make_first max len sum =
   1.183  			if sum<=max orelse max<0 then
   1.184 -				apsome (fn xs' => sum :: xs') (make_first max (len-1) 0)
   1.185 +				Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0)
   1.186  			else
   1.187 -				apsome (fn xs' => max :: xs') (make_first max (len-1) (sum-max))
   1.188 +				Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max))
   1.189  		(* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
   1.190  		(* all list elements x (unless 'max'<0)                                *)
   1.191  		(* int -> int -> int -> int list -> int list option *)
   1.192 @@ -867,12 +867,12 @@
   1.193  		  | next max len sum (x1::x2::xs) =
   1.194  			if x1>0 andalso (x2<max orelse max<0) then
   1.195  				(* we can shift *)
   1.196 -				SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
   1.197 +				SOME (valOf (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
   1.198  			else
   1.199  				(* continue search *)
   1.200  				next max (len+1) (sum+x1) (x2::xs)
   1.201  		(* only consider those types for which the size is not fixed *)
   1.202 -		val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) xs
   1.203 +		val mutables = List.filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) xs
   1.204  		(* subtract 'minsize' from every size (will be added again at the end) *)
   1.205  		val diffs = map (fn (_, n) => n-minsize) mutables
   1.206  	in
   1.207 @@ -931,7 +931,7 @@
   1.208  			(* Term.term list *)
   1.209  			val axioms = collect_axioms thy t
   1.210  			(* Term.typ list *)
   1.211 -			val types  = foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms)
   1.212 +			val types  = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms)
   1.213  			val _      = writeln ("Ground types: "
   1.214  				^ (if null types then "none."
   1.215  				   else commas (map (Sign.string_of_typ (sign_of thy)) types)))
   1.216 @@ -945,7 +945,7 @@
   1.217  						let
   1.218  							val index           = #index info
   1.219  							val descr           = #descr info
   1.220 -							val (_, _, constrs) = (the o assoc) (descr, index)
   1.221 +							val (_, _, constrs) = (valOf o assoc) (descr, index)
   1.222  						in
   1.223  							(* recursive datatype? *)
   1.224  							Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs
   1.225 @@ -1053,7 +1053,7 @@
   1.226  		(* (Term.indexname * Term.typ) list *)
   1.227  		val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   1.228  		(* Term.term *)
   1.229 -		val ex_closure = foldl
   1.230 +		val ex_closure = Library.foldl
   1.231  			(fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
   1.232  			(t, vars)
   1.233  		(* If 't' is of type 'propT' (rather than 'boolT'), applying  *)
   1.234 @@ -1075,7 +1075,7 @@
   1.235  	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
   1.236  
   1.237  	fun refute_subgoal thy params thm subgoal =
   1.238 -		refute_term thy params (nth_elem (subgoal, prems_of thm));
   1.239 +		refute_term thy params (List.nth (prems_of thm, subgoal));
   1.240  
   1.241  
   1.242  (* ------------------------------------------------------------------------- *)
   1.243 @@ -1116,7 +1116,7 @@
   1.244  			map (fn x => [x]) xs
   1.245  		  | pick_all n xs =
   1.246  			let val rec_pick = pick_all (n-1) xs in
   1.247 -				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   1.248 +				Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   1.249  			end
   1.250  	in
   1.251  		case intr of
   1.252 @@ -1269,7 +1269,7 @@
   1.253  			map (fn x => [x]) xs
   1.254  		  | pick_all (xs::xss) =
   1.255  			let val rec_pick = pick_all xss in
   1.256 -				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   1.257 +				Library.foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   1.258  			end
   1.259  		  | pick_all _ =
   1.260  			raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
   1.261 @@ -1296,8 +1296,8 @@
   1.262  	let
   1.263  		val Ts = binder_types (fastype_of t)
   1.264  	in
   1.265 -		foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
   1.266 -			(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
   1.267 +		Library.foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
   1.268 +			(Library.take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
   1.269  	end;
   1.270  
   1.271  (* ------------------------------------------------------------------------- *)
   1.272 @@ -1306,7 +1306,7 @@
   1.273  
   1.274  	(* int list -> int *)
   1.275  
   1.276 -	fun sum xs = foldl op+ (0, xs);
   1.277 +	fun sum xs = Library.foldl op+ (0, xs);
   1.278  
   1.279  (* ------------------------------------------------------------------------- *)
   1.280  (* product: returns the product of a list 'xs' of integers                   *)
   1.281 @@ -1314,7 +1314,7 @@
   1.282  
   1.283  	(* int list -> int *)
   1.284  
   1.285 -	fun product xs = foldl op* (1, xs);
   1.286 +	fun product xs = Library.foldl op* (1, xs);
   1.287  
   1.288  (* ------------------------------------------------------------------------- *)
   1.289  (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
   1.290 @@ -1354,7 +1354,7 @@
   1.291  			(* unit -> (interpretation * model * arguments) option *)
   1.292  			fun interpret_groundtype () =
   1.293  			let
   1.294 -				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))                    (* the model MUST specify a size for ground types *)
   1.295 +				val size = (if T = Term.propT then 2 else (valOf o assoc) (typs, T))                    (* the model MUST specify a size for ground types *)
   1.296  				val next = next_idx+size
   1.297  				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   1.298  				(* prop_formula list *)
   1.299 @@ -1416,7 +1416,7 @@
   1.300  			| Var (_, T)       =>
   1.301  				interpret_groundterm T
   1.302  			| Bound i          =>
   1.303 -				SOME (nth_elem (i, #bounds args), model, args)
   1.304 +				SOME (List.nth (#bounds args, i), model, args)
   1.305  			| Abs (x, T, body) =>
   1.306  				let
   1.307  					(* create all constants of type 'T' *)
   1.308 @@ -1656,7 +1656,7 @@
   1.309  						let
   1.310  							val index               = #index info
   1.311  							val descr               = #descr info
   1.312 -							val (_, dtyps, constrs) = (the o assoc) (descr, index)
   1.313 +							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.314  							val typ_assoc           = dtyps ~~ Ts
   1.315  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.316  							val _ = (if Library.exists (fn d =>
   1.317 @@ -1723,7 +1723,7 @@
   1.318  						let
   1.319  							val index               = #index info
   1.320  							val descr               = #descr info
   1.321 -							val (_, dtyps, constrs) = (the o assoc) (descr, index)
   1.322 +							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.323  							val typ_assoc           = dtyps ~~ Ts'
   1.324  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.325  							val _ = (if Library.exists (fn d =>
   1.326 @@ -1846,7 +1846,7 @@
   1.327  									(* after it generate further elements                                    *)
   1.328  									val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 +
   1.329  										(if is_rec_constr ctypes then
   1.330 -											size_of_dtyp thy typs' descr typ_assoc (filter (not o is_rec_constr o snd) cs)
   1.331 +											size_of_dtyp thy typs' descr typ_assoc (List.filter (not o is_rec_constr o snd) cs)
   1.332  										else
   1.333  											0)
   1.334  								in
   1.335 @@ -1904,7 +1904,7 @@
   1.336  						let
   1.337  							val index               = #index info
   1.338  							val descr               = #descr info
   1.339 -							val (_, dtyps, constrs) = (the o assoc) (descr, index)
   1.340 +							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.341  							(* the total number of constructors, including those of different    *)
   1.342  							(* (mutually recursive) datatypes within the same descriptor 'descr' *)
   1.343  							val constrs_count = sum (map (fn (_, (_, _, cs)) => length cs) descr)
   1.344 @@ -1931,7 +1931,7 @@
   1.345  										end) ((model, args), params)
   1.346  									val (typs, terms) = model'
   1.347  									(* the type of a recursion operator: [T1, ..., Tn, IDT] ---> Tresult *)
   1.348 -									val IDT       = nth_elem (constrs_count, binder_types T)
   1.349 +									val IDT       = List.nth (binder_types T, constrs_count)
   1.350  									val typ_assoc = dtyps ~~ (snd o dest_Type) IDT
   1.351  									(* interpret each constructor of the datatype *)
   1.352  									(* TODO: we probably need to interpret every constructor in the descriptor, *)
   1.353 @@ -1993,13 +1993,13 @@
   1.354  												  | select_subtree (Leaf _, _) =
   1.355  													raise REFUTE ("IDT_recursion_interpreter", "interpretation for parameter is a leaf; cannot select a subtree")
   1.356  												  | select_subtree (Node tr, x::xs) =
   1.357 -													select_subtree (nth_elem (x, tr), xs)
   1.358 +													select_subtree (List.nth (tr, x), xs)
   1.359  												(* select the correct subtree of the parameter corresponding to constructor 'c' *)
   1.360 -												val p_intr = select_subtree (nth_elem (c, p_intrs), args)
   1.361 +												val p_intr = select_subtree (List.nth (p_intrs, c), args)
   1.362  												(* find the indices of recursive arguments *)
   1.363 -												val rec_args = map snd (filter (DatatypeAux.is_rec_type o fst) ((snd (nth_elem (c, constrs))) ~~ args))
   1.364 +												val rec_args = map snd (List.filter (DatatypeAux.is_rec_type o fst) ((snd (List.nth (constrs, c))) ~~ args))
   1.365  												(* apply 'p_intr' to recursively computed results *)
   1.366 -												val rec_p_intr = foldl (fn (i, n) => interpretation_apply (i, Array.sub (INTRS, n))) (p_intr, rec_args)
   1.367 +												val rec_p_intr = Library.foldl (fn (i, n) => interpretation_apply (i, Array.sub (INTRS, n))) (p_intr, rec_args)
   1.368  												(* update 'INTRS' *)
   1.369  												val _ = Array.update (INTRS, elem, rec_p_intr)
   1.370  											in
   1.371 @@ -2036,7 +2036,7 @@
   1.372  				val constants     = make_constants i_set
   1.373  				(* interpretation -> int *)
   1.374  				fun number_of_elements (Node xs) =
   1.375 -					foldl (fn (n, x) =>
   1.376 +					Library.foldl (fn (n, x) =>
   1.377  						if x=TT then
   1.378  							n+1
   1.379  						else if x=FF then
   1.380 @@ -2214,7 +2214,7 @@
   1.381  					val HOLogic_empty_set = Const ("{}", HOLogic_setT)
   1.382  					val HOLogic_insert    = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   1.383  				in
   1.384 -					SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
   1.385 +					SOME (Library.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
   1.386  				end
   1.387  			| Type ("prop", [])      =>
   1.388  				(case index_from_interpretation intr of
   1.389 @@ -2259,7 +2259,7 @@
   1.390  					  Node xs => xs
   1.391  					| _       => raise REFUTE ("set_printer", "interpretation for set type is a leaf"))
   1.392  				(* Term.term list *)
   1.393 -				val elements = mapfilter (fn (arg, result) =>
   1.394 +				val elements = List.mapPartial (fn (arg, result) =>
   1.395  					case result of
   1.396  					  Leaf [fmTrue, fmFalse] =>
   1.397  						if PropLogic.eval assignment fmTrue then
   1.398 @@ -2275,7 +2275,7 @@
   1.399  				val HOLogic_empty_set = Const ("{}", HOLogic_setT)
   1.400  				val HOLogic_insert    = Const ("insert", T --> HOLogic_setT --> HOLogic_setT)
   1.401  			in
   1.402 -				SOME (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
   1.403 +				SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
   1.404  			end
   1.405  		| _ =>
   1.406  			NONE
   1.407 @@ -2299,7 +2299,7 @@
   1.408  					val (typs, _)           = model
   1.409  					val index               = #index info
   1.410  					val descr               = #descr info
   1.411 -					val (_, dtyps, constrs) = (the o assoc) (descr, index)
   1.412 +					val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
   1.413  					val typ_assoc           = dtyps ~~ Ts
   1.414  					(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.415  					val _ = (if Library.exists (fn d =>
   1.416 @@ -2345,7 +2345,7 @@
   1.417  										search (xs, 0)
   1.418  									end
   1.419  							in
   1.420 -								apsome (fn args => (cTerm, cargs, args)) (get_args iC)
   1.421 +								Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
   1.422  							end
   1.423  						(* Term.term * DatatypeAux.dtyp list * int list *)
   1.424  						val (cTerm, cargs, args) = (case get_first get_constr_args constrs of
   1.425 @@ -2359,10 +2359,10 @@
   1.426  									(* list, so there might be a more efficient implementation that does    *)
   1.427  									(* not generate all constants                                           *)
   1.428  							in
   1.429 -								print thy (typs, []) (Free ("dummy", dT)) (nth_elem (n, consts)) assignment
   1.430 +								print thy (typs, []) (Free ("dummy", dT)) (List.nth (consts, n)) assignment
   1.431  							end) (cargs ~~ args)
   1.432  					in
   1.433 -						SOME (foldl op$ (cTerm, argsTerms))
   1.434 +						SOME (Library.foldl op$ (cTerm, argsTerms))
   1.435  					end
   1.436  				end
   1.437  			| NONE =>  (* not an inductive datatype *)