src/HOL/Tools/refute.ML
changeset 15531 08c8dad8e399
parent 15335 f81e6e24351f
child 15547 f08e2d83681e
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -213,8 +213,8 @@
     1.4  
     1.5  	fun interpret thy model args t =
     1.6  		(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
     1.7 -		  None   => raise REFUTE ("interpret", "unable to interpret term " ^ quote (Sign.string_of_term (sign_of thy) t))
     1.8 -		| Some x => x);
     1.9 +		  NONE   => raise REFUTE ("interpret", "unable to interpret term " ^ quote (Sign.string_of_term (sign_of thy) t))
    1.10 +		| SOME x => x);
    1.11  
    1.12  (* ------------------------------------------------------------------------- *)
    1.13  (* print: tries to convert the constant denoted by the term 't' into a term  *)
    1.14 @@ -225,8 +225,8 @@
    1.15  
    1.16  	fun print thy model t intr assignment =
    1.17  		(case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
    1.18 -		  None   => Const ("<<no printer available>>", fastype_of t)
    1.19 -		| Some x => x);
    1.20 +		  NONE   => Const ("<<no printer available>>", fastype_of t)
    1.21 +		| SOME x => x);
    1.22  
    1.23  (* ------------------------------------------------------------------------- *)
    1.24  (* print_model: turns the model into a string, using a fixed interpretation  *)
    1.25 @@ -256,9 +256,9 @@
    1.26  				space_implode "\n" (mapfilter (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 +						SOME (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment))
    1.31  					else
    1.32 -						None) terms) ^ "\n"
    1.33 +						NONE) terms) ^ "\n"
    1.34  	in
    1.35  		typs_msg ^ show_consts_msg ^ terms_msg
    1.36  	end;
    1.37 @@ -275,8 +275,8 @@
    1.38  		val {interpreters, printers, parameters} = RefuteData.get thy
    1.39  	in
    1.40  		case assoc (interpreters, name) of
    1.41 -		  None   => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
    1.42 -		| Some _ => error ("Interpreter " ^ name ^ " already declared")
    1.43 +		  NONE   => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
    1.44 +		| SOME _ => error ("Interpreter " ^ name ^ " already declared")
    1.45  	end;
    1.46  
    1.47  	(* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory *)
    1.48 @@ -286,8 +286,8 @@
    1.49  		val {interpreters, printers, parameters} = RefuteData.get thy
    1.50  	in
    1.51  		case assoc (printers, name) of
    1.52 -		  None   => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
    1.53 -		| Some _ => error ("Printer " ^ name ^ " already declared")
    1.54 +		  NONE   => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
    1.55 +		| SOME _ => error ("Printer " ^ name ^ " already declared")
    1.56  	end;
    1.57  
    1.58  (* ------------------------------------------------------------------------- *)
    1.59 @@ -302,9 +302,9 @@
    1.60  		val {interpreters, printers, parameters} = RefuteData.get thy
    1.61  	in
    1.62  		case Symtab.lookup (parameters, name) of
    1.63 -		  None   => RefuteData.put
    1.64 +		  NONE   => RefuteData.put
    1.65  			{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
    1.66 -		| Some _ => RefuteData.put
    1.67 +		| SOME _ => RefuteData.put
    1.68  			{interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy
    1.69  	end;
    1.70  
    1.71 @@ -339,15 +339,15 @@
    1.72  		(* (string * string) list * string -> int *)
    1.73  		fun read_int (parms, name) =
    1.74  			case assoc_string (parms, name) of
    1.75 -			  Some s => (case Int.fromString s of
    1.76 +			  SOME s => (case Int.fromString s of
    1.77  				  SOME i => i
    1.78  				| NONE   => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
    1.79 -			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
    1.80 +			| NONE   => error ("parameter " ^ quote name ^ " must be assigned a value")
    1.81  		(* (string * string) list * string -> string *)
    1.82  		fun read_string (parms, name) =
    1.83  			case assoc_string (parms, name) of
    1.84 -			  Some s => s
    1.85 -			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
    1.86 +			  SOME s => s
    1.87 +			| NONE   => error ("parameter " ^ quote name ^ " must be assigned a value")
    1.88  		(* (string * string) list *)
    1.89  		val allparams = override @ (get_default_params thy)  (* 'override' first, defaults last *)
    1.90  		(* int *)
    1.91 @@ -363,7 +363,7 @@
    1.92  		(*       whose name is one of the other parameters (e.g. 'maxvars')    *)
    1.93  		(* (string * int) list *)
    1.94  		val sizes     = mapfilter
    1.95 -			(fn (name,value) => (case Int.fromString value of SOME i => Some (name, i) | NONE => None))
    1.96 +			(fn (name,value) => (case Int.fromString value of SOME i => SOME (name, i) | NONE => NONE))
    1.97  			(filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver")
    1.98  				allparams)
    1.99  	in
   1.100 @@ -431,27 +431,27 @@
   1.101  		let
   1.102  			fun find_typeSubs (Const (s', T')) =
   1.103  				(if s=s' then
   1.104 -					Some (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T)))
   1.105 +					SOME (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T)))
   1.106  				else
   1.107 -					None
   1.108 -				handle Type.TYPE_MATCH => None)
   1.109 -			  | find_typeSubs (Free _)           = None
   1.110 -			  | find_typeSubs (Var _)            = None
   1.111 -			  | find_typeSubs (Bound _)          = None
   1.112 +					NONE
   1.113 +				handle Type.TYPE_MATCH => NONE)
   1.114 +			  | find_typeSubs (Free _)           = NONE
   1.115 +			  | find_typeSubs (Var _)            = NONE
   1.116 +			  | find_typeSubs (Bound _)          = NONE
   1.117  			  | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
   1.118 -			  | find_typeSubs (t1 $ t2)          = (case find_typeSubs t1 of Some x => Some x | None => find_typeSubs t2)
   1.119 +			  | find_typeSubs (t1 $ t2)          = (case find_typeSubs t1 of SOME x => SOME x | NONE => find_typeSubs t2)
   1.120  			val typeSubs = (case find_typeSubs t of
   1.121 -				  Some x => x
   1.122 -				| None   => raise REFUTE ("collect_axioms", "no type instantiation found for " ^ quote s ^ " in " ^ Sign.string_of_term (sign_of thy) t))
   1.123 +				  SOME x => x
   1.124 +				| NONE   => raise REFUTE ("collect_axioms", "no type instantiation found for " ^ quote s ^ " in " ^ Sign.string_of_term (sign_of thy) t))
   1.125  		in
   1.126  			map_term_types
   1.127  				(map_type_tvar
   1.128  					(fn (v,_) =>
   1.129  						case Vartab.lookup (typeSubs, v) of
   1.130 -						  None =>
   1.131 +						  NONE =>
   1.132  							(* schematic type variable not instantiated *)
   1.133  							raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")")
   1.134 -						| Some typ =>
   1.135 +						| SOME typ =>
   1.136  							typ))
   1.137  					t
   1.138  		end
   1.139 @@ -462,10 +462,10 @@
   1.140  			map_term_types (map_type_tvar
   1.141  				(fn (v,_) =>
   1.142  					case Vartab.lookup (typeSubs, v) of
   1.143 -					  None =>
   1.144 +					  NONE =>
   1.145  						(* schematic type variable not instantiated *)
   1.146  						raise ERROR
   1.147 -					| Some typ =>
   1.148 +					| SOME typ =>
   1.149  						typ)) t
   1.150  		(* Term.term list * Term.typ -> Term.term list *)
   1.151  		fun collect_type_axioms (axs, T) =
   1.152 @@ -479,30 +479,30 @@
   1.153  					(* look up the definition of a type, as created by "typedef" *)
   1.154  					(* (string * Term.term) list -> (string * Term.term) option *)
   1.155  					fun get_typedefn [] =
   1.156 -						None
   1.157 +						NONE
   1.158  					  | get_typedefn ((axname,ax)::axms) =
   1.159  						(let
   1.160  							(* Term.term -> Term.typ option *)
   1.161  							fun type_of_type_definition (Const (s', T')) =
   1.162  								if s'="Typedef.type_definition" then
   1.163 -									Some T'
   1.164 +									SOME T'
   1.165  								else
   1.166 -									None
   1.167 -							  | type_of_type_definition (Free _)           = None
   1.168 -							  | type_of_type_definition (Var _)            = None
   1.169 -							  | type_of_type_definition (Bound _)          = None
   1.170 +									NONE
   1.171 +							  | type_of_type_definition (Free _)           = NONE
   1.172 +							  | type_of_type_definition (Var _)            = NONE
   1.173 +							  | type_of_type_definition (Bound _)          = NONE
   1.174  							  | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body
   1.175 -							  | type_of_type_definition (t1 $ t2)          = (case type_of_type_definition t1 of Some x => Some x | None => type_of_type_definition t2)
   1.176 +							  | type_of_type_definition (t1 $ t2)          = (case type_of_type_definition t1 of SOME x => SOME x | NONE => type_of_type_definition t2)
   1.177  						in
   1.178  							case type_of_type_definition ax of
   1.179 -							  Some T' =>
   1.180 +							  SOME T' =>
   1.181  								let
   1.182  									val T''      = (domain_type o domain_type) T'
   1.183  									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
   1.184  								in
   1.185 -									Some (axname, monomorphic_term typeSubs ax)
   1.186 +									SOME (axname, monomorphic_term typeSubs ax)
   1.187  								end
   1.188 -							| None =>
   1.189 +							| NONE =>
   1.190  								get_typedefn axms
   1.191  						end
   1.192  						handle ERROR           => get_typedefn axms
   1.193 @@ -510,19 +510,19 @@
   1.194  						     | Type.TYPE_MATCH => get_typedefn axms)
   1.195  				in
   1.196  					case DatatypePackage.datatype_info thy s of
   1.197 -					  Some info =>  (* inductive datatype *)
   1.198 +					  SOME info =>  (* inductive datatype *)
   1.199  							(* only collect relevant type axioms for the argument types *)
   1.200  							foldl collect_type_axioms (axs, Ts)
   1.201 -					| None =>
   1.202 +					| NONE =>
   1.203  						(case get_typedefn axioms of
   1.204 -						  Some (axname, ax) => 
   1.205 +						  SOME (axname, ax) => 
   1.206  							if mem_term (ax, axs) then
   1.207  								(* collect relevant type axioms for the argument types *)
   1.208  								foldl collect_type_axioms (axs, Ts)
   1.209  							else
   1.210  								(immediate_output (" " ^ axname);
   1.211  								collect_term_axioms (ax :: axs, ax))
   1.212 -						| None =>
   1.213 +						| NONE =>
   1.214  							(* at least collect relevant type axioms for the argument types *)
   1.215  							foldl collect_type_axioms (axs, Ts))
   1.216  				end
   1.217 @@ -579,7 +579,7 @@
   1.218  					(* look up the definition of a constant, as created by "constdefs" *)
   1.219  					(* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *)
   1.220  					fun get_defn [] =
   1.221 -						None
   1.222 +						NONE
   1.223  					  | get_defn ((axname,ax)::axms) =
   1.224  						(let
   1.225  							val (lhs, _) = Logic.dest_equals ax  (* equations only *)
   1.226 @@ -590,7 +590,7 @@
   1.227  								let
   1.228  									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
   1.229  								in
   1.230 -									Some (axname, monomorphic_term typeSubs ax)
   1.231 +									SOME (axname, monomorphic_term typeSubs ax)
   1.232  								end
   1.233  							else
   1.234  								get_defn axms
   1.235 @@ -603,7 +603,7 @@
   1.236  							(case body_type T of
   1.237  							  Type (s', _) =>
   1.238  								(case DatatypePackage.constrs_of thy s' of
   1.239 -								  Some constrs =>
   1.240 +								  SOME constrs =>
   1.241  									Library.exists (fn c =>
   1.242  										(case c of
   1.243  										  Const (cname, ctype) =>
   1.244 @@ -611,7 +611,7 @@
   1.245  										| _ =>
   1.246  											raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
   1.247  										constrs
   1.248 -								| None =>
   1.249 +								| NONE =>
   1.250  									false)
   1.251  							| _  =>
   1.252  								false)
   1.253 @@ -622,8 +622,8 @@
   1.254  							((case last_elem (binder_types T) of
   1.255  							  Type (s', _) =>
   1.256  								(case DatatypePackage.datatype_info thy s' of
   1.257 -								  Some info => s mem (#rec_names info)
   1.258 -								| None      => false)  (* not an inductive datatype *)
   1.259 +								  SOME info => s mem (#rec_names info)
   1.260 +								| NONE      => false)  (* not an inductive datatype *)
   1.261  							| _ =>  (* a (free or schematic) type variable *)
   1.262  								false)
   1.263  							handle LIST "last_elem" => false)  (* not even a function type *)
   1.264 @@ -641,14 +641,14 @@
   1.265  						collect_type_axioms (axs, T)
   1.266  					) else
   1.267  						(case get_defn axioms of
   1.268 -						  Some (axname, ax) => 
   1.269 +						  SOME (axname, ax) => 
   1.270  							if mem_term (ax, axs) then
   1.271  								(* collect relevant type axioms *)
   1.272  								collect_type_axioms (axs, T)
   1.273  							else
   1.274  								(immediate_output (" " ^ axname);
   1.275  								collect_term_axioms (ax :: axs, ax))
   1.276 -						| None =>
   1.277 +						| NONE =>
   1.278  							(* collect relevant type axioms *)
   1.279  							collect_type_axioms (axs, T))
   1.280  				end
   1.281 @@ -698,7 +698,7 @@
   1.282  				| Type ("set", [T1])     => collect_types (T1, acc)
   1.283  				| Type (s, Ts)           =>
   1.284  					(case DatatypePackage.datatype_info thy s of
   1.285 -					  Some info =>  (* inductive datatype *)
   1.286 +					  SOME info =>  (* inductive datatype *)
   1.287  						let
   1.288  							val index               = #index info
   1.289  							val descr               = #descr info
   1.290 @@ -723,7 +723,7 @@
   1.291  						in
   1.292  							acc_constrs
   1.293  						end
   1.294 -					| None =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
   1.295 +					| NONE =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
   1.296  						T ins (foldr collect_types (Ts, acc)))
   1.297  				| TFree _                => T ins acc
   1.298  				| TVar _                 => T ins acc)
   1.299 @@ -756,8 +756,8 @@
   1.300  	let
   1.301  		fun size_of_typ T =
   1.302  			case assoc (sizes, string_of_typ T) of
   1.303 -			  Some n => n
   1.304 -			| None   => minsize
   1.305 +			  SOME n => n
   1.306 +			| NONE   => minsize
   1.307  	in
   1.308  		map (fn T => (T, size_of_typ T)) xs
   1.309  	end;
   1.310 @@ -775,15 +775,15 @@
   1.311  	let
   1.312  		(* int -> int list -> int list option *)
   1.313  		fun add1 _ [] =
   1.314 -			None  (* overflow *)
   1.315 +			NONE  (* overflow *)
   1.316  		  | add1 max (x::xs) =
   1.317  		 	if x<max orelse max<0 then
   1.318 -				Some ((x+1)::xs)  (* add 1 to the head *)
   1.319 +				SOME ((x+1)::xs)  (* add 1 to the head *)
   1.320  			else
   1.321  				apsome (fn xs' => 0 :: xs') (add1 max xs)  (* carry-over *)
   1.322  		(* int -> int list * int list -> int list option *)
   1.323  		fun shift _ (_, []) =
   1.324 -			None
   1.325 +			NONE
   1.326  		  | shift max (zeros, x::xs) =
   1.327  			if x=0 then
   1.328  				shift max (0::zeros, xs)
   1.329 @@ -794,9 +794,9 @@
   1.330  		(* int -> int -> int -> int list option *)
   1.331  		fun make_first 0 sum _ =
   1.332  			if sum=0 then
   1.333 -				Some []
   1.334 +				SOME []
   1.335  			else
   1.336 -				None
   1.337 +				NONE
   1.338  		  | make_first len sum max =
   1.339  			if sum<=max orelse max<0 then
   1.340  				apsome (fn xs' => sum :: xs') (make_first (len-1) 0 max)
   1.341 @@ -807,29 +807,29 @@
   1.342  		(* int -> int list -> int list option *)
   1.343  		fun next max xs =
   1.344  			(case shift max ([], xs) of
   1.345 -			  Some xs' =>
   1.346 -				Some xs'
   1.347 -			| None =>
   1.348 +			  SOME xs' =>
   1.349 +				SOME xs'
   1.350 +			| NONE =>
   1.351  				let
   1.352  					val (len, sum) = foldl (fn ((l, s), x) => (l+1, s+x)) ((0, 0), xs)
   1.353  				in
   1.354  					make_first len (sum+1) max  (* increment 'sum' by 1 *)
   1.355  				end)
   1.356  		(* only consider those types for which the size is not fixed *)
   1.357 -		val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = None) xs
   1.358 +		val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) xs
   1.359  		(* subtract 'minsize' from every size (will be added again at the end) *)
   1.360  		val diffs = map (fn (_, n) => n-minsize) mutables
   1.361  	in
   1.362  		case next (maxsize-minsize) diffs of
   1.363 -		  Some diffs' =>
   1.364 +		  SOME diffs' =>
   1.365  			(* merge with those types for which the size is fixed *)
   1.366 -			Some (snd (foldl_map (fn (ds, (T, _)) =>
   1.367 +			SOME (snd (foldl_map (fn (ds, (T, _)) =>
   1.368  				case assoc (sizes, string_of_typ T) of
   1.369 -				  Some n => (ds, (T, n))                      (* return the fixed size *)
   1.370 -				| None   => (tl ds, (T, minsize + (hd ds))))  (* consume the head of 'ds', add 'minsize' *)
   1.371 +				  SOME n => (ds, (T, n))                      (* return the fixed size *)
   1.372 +				| NONE   => (tl ds, (T, minsize + (hd ds))))  (* consume the head of 'ds', add 'minsize' *)
   1.373  				(diffs', xs)))
   1.374 -		| None =>
   1.375 -			None
   1.376 +		| NONE =>
   1.377 +			NONE
   1.378  	end;
   1.379  
   1.380  (* ------------------------------------------------------------------------- *)
   1.381 @@ -901,12 +901,12 @@
   1.382  				immediate_output " invoking SAT solver...";
   1.383  				(case SatSolver.invoke_solver satsolver fm of
   1.384  				  SatSolver.SATISFIABLE assignment =>
   1.385 -					writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b | None => true))
   1.386 +					writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of SOME b => b | NONE => true))
   1.387  				| _ =>  (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *)
   1.388  					(immediate_output " no model found.\n";
   1.389  					case next_universe universe sizes minsize maxsize of
   1.390 -					  Some universe' => find_model_loop universe'
   1.391 -					| None           => writeln "Search terminated, no larger universe within the given limits."))
   1.392 +					  SOME universe' => find_model_loop universe'
   1.393 +					| NONE           => writeln "Search terminated, no larger universe within the given limits."))
   1.394  				handle SatSolver.NOT_CONFIGURED =>
   1.395  					error ("SAT solver " ^ quote satsolver ^ " is not configured.")
   1.396  			end handle MAXVARS_EXCEEDED =>
   1.397 @@ -1207,7 +1207,7 @@
   1.398  				val wf   = (if size=1 then True else if size=2 then True else exactly_one_true fms)
   1.399  			in
   1.400  				(* extend the model, increase 'next_idx', add well-formedness condition *)
   1.401 -				Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.402 +				SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.403  			end
   1.404  		in
   1.405  			case T of
   1.406 @@ -1235,7 +1235,7 @@
   1.407  					val intr = Node copies
   1.408  				in
   1.409  					(* extend the model, increase 'next_idx', add well-formedness condition *)
   1.410 -					Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.411 +					SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.412  				end
   1.413  			| Type _  => interpret_groundtype ()
   1.414  			| TFree _ => interpret_groundtype ()
   1.415 @@ -1243,10 +1243,10 @@
   1.416  		end
   1.417  	in
   1.418  		case assoc (terms, t) of
   1.419 -		  Some intr =>
   1.420 +		  SOME intr =>
   1.421  			(* return an existing interpretation *)
   1.422 -			Some (intr, model, args)
   1.423 -		| None =>
   1.424 +			SOME (intr, model, args)
   1.425 +		| NONE =>
   1.426  			(case t of
   1.427  			  Const (_, T)     =>
   1.428  				interpret_groundterm T
   1.429 @@ -1255,7 +1255,7 @@
   1.430  			| Var (_, T)       =>
   1.431  				interpret_groundterm T
   1.432  			| Bound i          =>
   1.433 -				Some (nth_elem (i, #bounds args), model, args)
   1.434 +				SOME (nth_elem (i, #bounds args), model, args)
   1.435  			| Abs (x, T, body) =>
   1.436  				let
   1.437  					(* create all constants of type 'T' *)
   1.438 @@ -1273,7 +1273,7 @@
   1.439  							end)
   1.440  						((model, args), constants)
   1.441  				in
   1.442 -					Some (Node bodies, model', args')
   1.443 +					SOME (Node bodies, model', args')
   1.444  				end
   1.445  			| t1 $ t2          =>
   1.446  				let
   1.447 @@ -1321,7 +1321,7 @@
   1.448  					val (intr1, model1, args1) = interpret thy model args t1
   1.449  					val (intr2, model2, args2) = interpret thy model1 args1 t2
   1.450  				in
   1.451 -					Some (interpretation_apply (intr1,intr2), model2, args2)
   1.452 +					SOME (interpretation_apply (intr1,intr2), model2, args2)
   1.453  				end)
   1.454  	end;
   1.455  
   1.456 @@ -1339,7 +1339,7 @@
   1.457  						val fmTrue  = PropLogic.all (map toTrue xs)
   1.458  						val fmFalse = PropLogic.exists (map toFalse xs)
   1.459  					in
   1.460 -						Some (Leaf [fmTrue, fmFalse], m, a)
   1.461 +						SOME (Leaf [fmTrue, fmFalse], m, a)
   1.462  					end
   1.463  				| _ =>
   1.464  					raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
   1.465 @@ -1349,11 +1349,11 @@
   1.466  				val (i1, m1, a1) = interpret thy model args t1
   1.467  				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.468  			in
   1.469 -				Some (make_equality (i1, i2), m2, a2)
   1.470 +				SOME (make_equality (i1, i2), m2, a2)
   1.471  			end
   1.472  		| Const ("==>", _) =>  (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *)
   1.473 -			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
   1.474 -		| _ => None;
   1.475 +			SOME (Node [Node [TT, FF], Node [TT, TT]], model, args)
   1.476 +		| _ => NONE;
   1.477  
   1.478  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.479  
   1.480 @@ -1366,13 +1366,13 @@
   1.481  	(* ------------------------------------------------------------------------- *)
   1.482  		case t of
   1.483  		  Const ("Trueprop", _) =>
   1.484 -			Some (Node [TT, FF], model, args)
   1.485 +			SOME (Node [TT, FF], model, args)
   1.486  		| Const ("Not", _) =>
   1.487 -			Some (Node [FF, TT], model, args)
   1.488 +			SOME (Node [FF, TT], model, args)
   1.489  		| Const ("True", _) =>  (* redundant, since 'True' is also an IDT constructor *)
   1.490 -			Some (TT, model, args)
   1.491 +			SOME (TT, model, args)
   1.492  		| Const ("False", _) =>  (* redundant, since 'False' is also an IDT constructor *)
   1.493 -			Some (FF, model, args)
   1.494 +			SOME (FF, model, args)
   1.495  		| Const ("All", _) $ t1 =>
   1.496  		(* if "All" occurs without an argument (i.e. as argument to a higher-order *)
   1.497  		(* function or  predicate), it is handled by the 'stlc_interpreter' (i.e.  *)
   1.498 @@ -1386,7 +1386,7 @@
   1.499  						val fmTrue  = PropLogic.all (map toTrue xs)
   1.500  						val fmFalse = PropLogic.exists (map toFalse xs)
   1.501  					in
   1.502 -						Some (Leaf [fmTrue, fmFalse], m, a)
   1.503 +						SOME (Leaf [fmTrue, fmFalse], m, a)
   1.504  					end
   1.505  				| _ =>
   1.506  					raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function")
   1.507 @@ -1404,7 +1404,7 @@
   1.508  						val fmTrue  = PropLogic.exists (map toTrue xs)
   1.509  						val fmFalse = PropLogic.all (map toFalse xs)
   1.510  					in
   1.511 -						Some (Leaf [fmTrue, fmFalse], m, a)
   1.512 +						SOME (Leaf [fmTrue, fmFalse], m, a)
   1.513  					end
   1.514  				| _ =>
   1.515  					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is followed by a non-function")
   1.516 @@ -1414,19 +1414,19 @@
   1.517  				val (i1, m1, a1) = interpret thy model args t1
   1.518  				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.519  			in
   1.520 -				Some (make_equality (i1, i2), m2, a2)
   1.521 +				SOME (make_equality (i1, i2), m2, a2)
   1.522  			end
   1.523  		| Const ("op =", _) $ t1 =>
   1.524 -			Some (interpret thy model args (eta_expand t 1))
   1.525 +			SOME (interpret thy model args (eta_expand t 1))
   1.526  		| Const ("op =", _) =>
   1.527 -			Some (interpret thy model args (eta_expand t 2))
   1.528 +			SOME (interpret thy model args (eta_expand t 2))
   1.529  		| Const ("op &", _) =>
   1.530 -			Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
   1.531 +			SOME (Node [Node [TT, FF], Node [FF, FF]], model, args)
   1.532  		| Const ("op |", _) =>
   1.533 -			Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
   1.534 +			SOME (Node [Node [TT, TT], Node [TT, FF]], model, args)
   1.535  		| Const ("op -->", _) =>
   1.536 -			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
   1.537 -		| _ => None;
   1.538 +			SOME (Node [Node [TT, FF], Node [TT, TT]], model, args)
   1.539 +		| _ => NONE;
   1.540  
   1.541  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.542  
   1.543 @@ -1436,42 +1436,42 @@
   1.544  		val (typs, terms) = model
   1.545  	in
   1.546  		case assoc (terms, t) of
   1.547 -		  Some intr =>
   1.548 +		  SOME intr =>
   1.549  			(* return an existing interpretation *)
   1.550 -			Some (intr, model, args)
   1.551 -		| None =>
   1.552 +			SOME (intr, model, args)
   1.553 +		| NONE =>
   1.554  			(case t of
   1.555  			  Free (x, Type ("set", [T])) =>
   1.556  				let
   1.557  					val (intr, _, args') = interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT))
   1.558  				in
   1.559 -					Some (intr, (typs, (t, intr)::terms), args')
   1.560 +					SOME (intr, (typs, (t, intr)::terms), args')
   1.561  				end
   1.562  			| Var ((x,i), Type ("set", [T])) =>
   1.563  				let
   1.564  					val (intr, _, args') = interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT))
   1.565  				in
   1.566 -					Some (intr, (typs, (t, intr)::terms), args')
   1.567 +					SOME (intr, (typs, (t, intr)::terms), args')
   1.568  				end
   1.569  			| Const (s, Type ("set", [T])) =>
   1.570  				let
   1.571  					val (intr, _, args') = interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT))
   1.572  				in
   1.573 -					Some (intr, (typs, (t, intr)::terms), args')
   1.574 +					SOME (intr, (typs, (t, intr)::terms), args')
   1.575  				end
   1.576  			(* 'Collect' == identity *)
   1.577  			| Const ("Collect", _) $ t1 =>
   1.578 -				Some (interpret thy model args t1)
   1.579 +				SOME (interpret thy model args t1)
   1.580  			| Const ("Collect", _) =>
   1.581 -				Some (interpret thy model args (eta_expand t 1))
   1.582 +				SOME (interpret thy model args (eta_expand t 1))
   1.583  			(* 'op :' == application *)
   1.584  			| Const ("op :", _) $ t1 $ t2 =>
   1.585 -				Some (interpret thy model args (t2 $ t1))
   1.586 +				SOME (interpret thy model args (t2 $ t1))
   1.587  			| Const ("op :", _) $ t1 =>
   1.588 -				Some (interpret thy model args (eta_expand t 1))
   1.589 +				SOME (interpret thy model args (eta_expand t 1))
   1.590  			| Const ("op :", _) =>
   1.591 -				Some (interpret thy model args (eta_expand t 2))
   1.592 -			| _ => None)
   1.593 +				SOME (interpret thy model args (eta_expand t 2))
   1.594 +			| _ => NONE)
   1.595  	end;
   1.596  
   1.597  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.598 @@ -1482,15 +1482,15 @@
   1.599  		(* Term.typ -> (interpretation * model * arguments) option *)
   1.600  		fun interpret_variable (Type (s, Ts)) =
   1.601  			(case DatatypePackage.datatype_info thy s of
   1.602 -			  Some info =>  (* inductive datatype *)
   1.603 +			  SOME info =>  (* inductive datatype *)
   1.604  				let
   1.605  					val (typs, terms) = model
   1.606  					(* int option -- only recursive IDTs have an associated depth *)
   1.607  					val depth         = assoc (typs, Type (s, Ts))
   1.608  				in
   1.609 -					if depth = (Some 0) then  (* termination condition to avoid infinite recursion *)
   1.610 +					if depth = (SOME 0) then  (* termination condition to avoid infinite recursion *)
   1.611  						(* return a leaf of size 0 *)
   1.612 -						Some (Leaf [], model, args)
   1.613 +						SOME (Leaf [], model, args)
   1.614  					else
   1.615  						let
   1.616  							val index               = #index info
   1.617 @@ -1505,7 +1505,7 @@
   1.618  								else
   1.619  									())
   1.620  							(* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
   1.621 -							val typs'    = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
   1.622 +							val typs'    = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s, Ts), n-1)))
   1.623  							(* recursively compute the size of the datatype *)
   1.624  							val size     = size_of_dtyp thy typs' descr typ_assoc constrs
   1.625  							val next_idx = #next_idx args
   1.626 @@ -1525,19 +1525,19 @@
   1.627  							val wf       = (if size=1 then True else if size=2 then True else exactly_one_true fms)
   1.628  						in
   1.629  							(* extend the model, increase 'next_idx', add well-formedness condition *)
   1.630 -							Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
   1.631 +							SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
   1.632  						end
   1.633  				end
   1.634 -			| None =>  (* not an inductive datatype *)
   1.635 -				None)
   1.636 +			| NONE =>  (* not an inductive datatype *)
   1.637 +				NONE)
   1.638  		  | interpret_variable _ =  (* a (free or schematic) type variable *)
   1.639 -			None
   1.640 +			NONE
   1.641  	in
   1.642  		case assoc (terms, t) of
   1.643 -		  Some intr =>
   1.644 +		  SOME intr =>
   1.645  			(* return an existing interpretation *)
   1.646 -			Some (intr, model, args)
   1.647 -		| None =>
   1.648 +			SOME (intr, model, args)
   1.649 +		| NONE =>
   1.650  			(case t of
   1.651  			  Free (_, T)  => interpret_variable T
   1.652  			| Var (_, T)   => interpret_variable T
   1.653 @@ -1549,7 +1549,7 @@
   1.654  						(case body_type T of
   1.655  						  Type (s', Ts') =>
   1.656  							(case DatatypePackage.datatype_info thy s' of
   1.657 -							  Some info =>  (* body type is an inductive datatype *)
   1.658 +							  SOME info =>  (* body type is an inductive datatype *)
   1.659  								let
   1.660  									val index               = #index info
   1.661  									val descr               = #descr info
   1.662 @@ -1570,12 +1570,12 @@
   1.663  									case constrs2 of
   1.664  									  [] =>
   1.665  										(* 'Const (s, T)' is not a constructor of this datatype *)
   1.666 -										None
   1.667 +										NONE
   1.668  									| c::cs =>
   1.669  										let
   1.670  											(* int option -- only recursive IDTs have an associated depth *)
   1.671  											val depth = assoc (typs, Type (s', Ts'))
   1.672 -											val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s', Ts'), n-1)))
   1.673 +											val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
   1.674  											(* constructors before 'Const (s, T)' generate elements of the datatype *)
   1.675  											val offset  = size_of_dtyp thy typs' descr typ_assoc constrs1
   1.676  											(* 'Const (s, T)' and constructors after it generate elements of the datatype *)
   1.677 @@ -1620,19 +1620,19 @@
   1.678  													(new_offset, Node (intrs @ (replicate (size-size') (make_partial ds))))
   1.679  												end
   1.680  										in
   1.681 -											Some ((snd o make_constr) (offset, snd c), model, args)
   1.682 +											SOME ((snd o make_constr) (offset, snd c), model, args)
   1.683  										end
   1.684  								end
   1.685 -							| None =>  (* body type is not an inductive datatype *)
   1.686 -								None)
   1.687 +							| NONE =>  (* body type is not an inductive datatype *)
   1.688 +								NONE)
   1.689  						| _ =>  (* body type is a (free or schematic) type variable *)
   1.690 -							None)
   1.691 +							NONE)
   1.692  				in
   1.693  					case interpret_constructor () of
   1.694 -					  Some x => Some x
   1.695 -					| None   => interpret_variable T
   1.696 +					  SOME x => SOME x
   1.697 +					| NONE   => interpret_variable T
   1.698  				end
   1.699 -			| _ => None)
   1.700 +			| _ => NONE)
   1.701  	end;
   1.702  
   1.703  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.704 @@ -1667,10 +1667,10 @@
   1.705  							Leaf (replicate size_nat False)
   1.706  					end
   1.707  			in
   1.708 -				Some (Node (map card constants), model, args)
   1.709 +				SOME (Node (map card constants), model, args)
   1.710  			end
   1.711  		| _ =>
   1.712 -			None;
   1.713 +			NONE;
   1.714  
   1.715  
   1.716  (* ------------------------------------------------------------------------- *)
   1.717 @@ -1682,10 +1682,10 @@
   1.718  	fun stlc_printer thy model t intr assignment =
   1.719  	let
   1.720  		(* Term.term -> Term.typ option *)
   1.721 -		fun typeof (Free (_, T))  = Some T
   1.722 -		  | typeof (Var (_, T))   = Some T
   1.723 -		  | typeof (Const (_, T)) = Some T
   1.724 -		  | typeof _              = None
   1.725 +		fun typeof (Free (_, T))  = SOME T
   1.726 +		  | typeof (Var (_, T))   = SOME T
   1.727 +		  | typeof (Const (_, T)) = SOME T
   1.728 +		  | typeof _              = NONE
   1.729  		(* string -> string *)
   1.730  		fun strip_leading_quote s =
   1.731  			(implode o (fn ss => case ss of [] => [] | x::xs => if x="'" then xs else ss) o explode) s
   1.732 @@ -1707,7 +1707,7 @@
   1.733  			raise REFUTE ("stlc_printer", "interpretation for ground type is not a leaf")
   1.734  	in
   1.735  		case typeof t of
   1.736 -		  Some T =>
   1.737 +		  SOME T =>
   1.738  			(case T of
   1.739  			  Type ("fun", [T1, T2]) =>
   1.740  				let
   1.741 @@ -1731,18 +1731,18 @@
   1.742  					val HOLogic_empty_set = Const ("{}", HOLogic_setT)
   1.743  					val HOLogic_insert    = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   1.744  				in
   1.745 -					Some (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
   1.746 +					SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
   1.747  				end
   1.748  			| Type ("prop", [])      =>
   1.749  				(case index_from_interpretation intr of
   1.750 -				  0 => Some (HOLogic.mk_Trueprop HOLogic.true_const)
   1.751 -				| 1 => Some (HOLogic.mk_Trueprop HOLogic.false_const)
   1.752 +				  0 => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
   1.753 +				| 1 => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
   1.754  				| _ => raise REFUTE ("stlc_interpreter", "illegal interpretation for a propositional value"))
   1.755 -			| Type _  => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
   1.756 -			| TFree _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
   1.757 -			| TVar _  => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)))
   1.758 -		| None =>
   1.759 -			None
   1.760 +			| Type _  => SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
   1.761 +			| TFree _ => SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
   1.762 +			| TVar _  => SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)))
   1.763 +		| NONE =>
   1.764 +			NONE
   1.765  	end;
   1.766  
   1.767  	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
   1.768 @@ -1750,13 +1750,13 @@
   1.769  	fun set_printer thy model t intr assignment =
   1.770  	let
   1.771  		(* Term.term -> Term.typ option *)
   1.772 -		fun typeof (Free (_, T))  = Some T
   1.773 -		  | typeof (Var (_, T))   = Some T
   1.774 -		  | typeof (Const (_, T)) = Some T
   1.775 -		  | typeof _              = None
   1.776 +		fun typeof (Free (_, T))  = SOME T
   1.777 +		  | typeof (Var (_, T))   = SOME T
   1.778 +		  | typeof (Const (_, T)) = SOME T
   1.779 +		  | typeof _              = NONE
   1.780  	in
   1.781  		case typeof t of
   1.782 -		  Some (Type ("set", [T])) =>
   1.783 +		  SOME (Type ("set", [T])) =>
   1.784  			let
   1.785  				(* create all constants of type 'T' *)
   1.786  				val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.787 @@ -1770,9 +1770,9 @@
   1.788  					case result of
   1.789  					  Leaf [fmTrue, fmFalse] =>
   1.790  						if PropLogic.eval assignment fmTrue then
   1.791 -							Some (print thy model (Free ("dummy", T)) arg assignment)
   1.792 +							SOME (print thy model (Free ("dummy", T)) arg assignment)
   1.793  						else if PropLogic.eval assignment fmFalse then
   1.794 -							None
   1.795 +							NONE
   1.796  						else
   1.797  							raise REFUTE ("set_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
   1.798  					| _ =>
   1.799 @@ -1784,10 +1784,10 @@
   1.800  				val HOLogic_empty_set = Const ("{}", HOLogic_setT)
   1.801  				val HOLogic_insert    = Const ("insert", T --> HOLogic_setT --> HOLogic_setT)
   1.802  			in
   1.803 -				Some (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
   1.804 +				SOME (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
   1.805  			end
   1.806  		| _ =>
   1.807 -			None
   1.808 +			NONE
   1.809  	end;
   1.810  
   1.811  	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *)
   1.812 @@ -1795,15 +1795,15 @@
   1.813  	fun IDT_printer thy model t intr assignment =
   1.814  	let
   1.815  		(* Term.term -> Term.typ option *)
   1.816 -		fun typeof (Free (_, T))  = Some T
   1.817 -		  | typeof (Var (_, T))   = Some T
   1.818 -		  | typeof (Const (_, T)) = Some T
   1.819 -		  | typeof _              = None
   1.820 +		fun typeof (Free (_, T))  = SOME T
   1.821 +		  | typeof (Var (_, T))   = SOME T
   1.822 +		  | typeof (Const (_, T)) = SOME T
   1.823 +		  | typeof _              = NONE
   1.824  	in
   1.825  		case typeof t of
   1.826 -		  Some (Type (s, Ts)) =>
   1.827 +		  SOME (Type (s, Ts)) =>
   1.828  			(case DatatypePackage.datatype_info thy s of
   1.829 -			  Some info =>  (* inductive datatype *)
   1.830 +			  SOME info =>  (* inductive datatype *)
   1.831  				let
   1.832  					val (typs, _)           = model
   1.833  					val index               = #index info
   1.834 @@ -1824,7 +1824,7 @@
   1.835  					val _ = (if element<0 then raise REFUTE ("IDT_printer", "invalid interpretation (no value assigned)") else ())
   1.836  					(* int option -- only recursive IDTs have an associated depth *)
   1.837  					val depth = assoc (typs, Type (s, Ts))
   1.838 -					val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
   1.839 +					val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s, Ts), n-1)))
   1.840  					(* int -> DatatypeAux.dtyp list -> Term.term list *)
   1.841  					fun make_args n [] =
   1.842  						if n<>0 then
   1.843 @@ -1860,12 +1860,12 @@
   1.844  								make_term (n-c_size) cs
   1.845  						end
   1.846  				in
   1.847 -					Some (make_term element constrs)
   1.848 +					SOME (make_term element constrs)
   1.849  				end
   1.850 -			| None =>  (* not an inductive datatype *)
   1.851 -				None)
   1.852 +			| NONE =>  (* not an inductive datatype *)
   1.853 +				NONE)
   1.854  		| _ =>  (* a (free or schematic) type variable *)
   1.855 -			None
   1.856 +			NONE
   1.857  	end;
   1.858  
   1.859