src/HOL/Import/shuffler.ML
changeset 15531 08c8dad8e399
parent 14854 61bdf2ae4dc5
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Import/shuffler.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4  	val res = (find_bound 0 body;2) handle RESULT i => i
     1.5      in
     1.6  	case res of
     1.7 -	    0 => Some (rew_th sg (x,xT) (y,yT) body)
     1.8 +	    0 => SOME (rew_th sg (x,xT) (y,yT) body)
     1.9  	  | 1 => if string_ord(y,x) = LESS
    1.10  		 then
    1.11  		     let
    1.12 @@ -239,12 +239,12 @@
    1.13  			 val t_th    = reflexive (cterm_of sg t)
    1.14  			 val newt_th = reflexive (cterm_of sg newt)
    1.15  		     in
    1.16 -			 Some (transitive t_th newt_th)
    1.17 +			 SOME (transitive t_th newt_th)
    1.18  		     end
    1.19 -		 else None
    1.20 +		 else NONE
    1.21  	  | _ => error "norm_term (quant_rewrite) internal error"
    1.22       end
    1.23 -  | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; None)
    1.24 +  | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE)
    1.25  
    1.26  fun freeze_thaw_term t =
    1.27      let
    1.28 @@ -304,7 +304,7 @@
    1.29  		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
    1.30  	    in
    1.31  		if not (lhs aconv origt)
    1.32 -		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.33 +		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.34  		      writeln (string_of_cterm (cterm_of sg origt));
    1.35  		      writeln (string_of_cterm (cterm_of sg lhs));
    1.36  		      writeln (string_of_cterm (cterm_of sg typet));
    1.37 @@ -338,15 +338,15 @@
    1.38  		      val res = final rew_th
    1.39  		      val lhs = (#1 (Logic.dest_equals (prop_of res)))
    1.40  		  in
    1.41 -		       Some res
    1.42 +		       SOME res
    1.43  		  end
    1.44 -	      else None)
    1.45 +	      else NONE)
    1.46  	     handle e => (writeln "eta_contract:";print_exn e))
    1.47 -	  | _ => (error ("Bad eta_contract argument" ^ (string_of_cterm (cterm_of sg t))); None)
    1.48 +	  | _ => (error ("Bad eta_contract argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
    1.49      end
    1.50  
    1.51  fun beta_fun sg assume t =
    1.52 -    Some (beta_conversion true (cterm_of sg t))
    1.53 +    SOME (beta_conversion true (cterm_of sg t))
    1.54  
    1.55  fun eta_expand sg assumes origt =
    1.56      let
    1.57 @@ -359,7 +359,7 @@
    1.58  		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
    1.59  	    in
    1.60  		if not (lhs aconv origt)
    1.61 -		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.62 +		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.63  		      writeln (string_of_cterm (cterm_of sg origt));
    1.64  		      writeln (string_of_cterm (cterm_of sg lhs));
    1.65  		      writeln (string_of_cterm (cterm_of sg typet));
    1.66 @@ -396,11 +396,11 @@
    1.67  			  val res = equal_intr th1 (th2' |> implies_intr concl)
    1.68  			  val res' = final res
    1.69  		      in
    1.70 -			  Some res'
    1.71 +			  SOME res'
    1.72  		      end
    1.73 -		    | _ => None)
    1.74 -	    else None
    1.75 -	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); None)
    1.76 +		    | _ => NONE)
    1.77 +	    else NONE
    1.78 +	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
    1.79      end
    1.80      handle e => (writeln "eta_expand internal error";print_exn e)
    1.81  
    1.82 @@ -519,19 +519,19 @@
    1.83      end
    1.84  
    1.85  (* make_equal sg t u tries to construct the theorem t == u under the
    1.86 -signature sg.  If it succeeds, Some (t == u) is returned, otherwise
    1.87 -None is returned. *)
    1.88 +signature sg.  If it succeeds, SOME (t == u) is returned, otherwise
    1.89 +NONE is returned. *)
    1.90  
    1.91  fun make_equal sg t u =
    1.92      let
    1.93  	val t_is_t' = norm_term sg t
    1.94  	val u_is_u' = norm_term sg u
    1.95  	val th = transitive t_is_t' (symmetric u_is_u')
    1.96 -	val _ = message ("make_equal: Some " ^ (string_of_thm th))
    1.97 +	val _ = message ("make_equal: SOME " ^ (string_of_thm th))
    1.98      in
    1.99 -	Some th
   1.100 +	SOME th
   1.101      end
   1.102 -    handle e as THM _ => (message "make_equal: None";None)
   1.103 +    handle e as THM _ => (message "make_equal: NONE";NONE)
   1.104  			 
   1.105  fun match_consts ignore t (* th *) =
   1.106      let
   1.107 @@ -564,7 +564,7 @@
   1.108  
   1.109  (* set_prop t thms tries to make a theorem with the proposition t from
   1.110  one of the theorems thms, by shuffling the propositions around.  If it
   1.111 -succeeds, Some theorem is returned, otherwise None.  *)
   1.112 +succeeds, SOME theorem is returned, otherwise NONE.  *)
   1.113  
   1.114  fun set_prop thy t =
   1.115      let
   1.116 @@ -576,34 +576,34 @@
   1.117  	val rhs = snd (dest_equals (cprop_of rew_th))
   1.118  
   1.119  	val shuffles = ShuffleData.get thy
   1.120 -	fun process [] = None
   1.121 +	fun process [] = NONE
   1.122  	  | process ((name,th)::thms) =
   1.123  	    let
   1.124  		val norm_th = varifyT (norm_thm thy (close_thm (transfer_sg sg th)))
   1.125  		val triv_th = trivial rhs
   1.126  		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
   1.127  		val mod_th = case Seq.pull (bicompose true (false,norm_th,0) 1 triv_th) of
   1.128 -				 Some(th,_) => Some th
   1.129 -			       | None => None
   1.130 +				 SOME(th,_) => SOME th
   1.131 +			       | NONE => NONE
   1.132  	    in
   1.133  		case mod_th of
   1.134 -		    Some mod_th =>
   1.135 +		    SOME mod_th =>
   1.136  		    let
   1.137  			val closed_th = equal_elim (symmetric rew_th) mod_th
   1.138  		    in
   1.139  			message ("Shuffler.set_prop succeeded by " ^ name);
   1.140 -			Some (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
   1.141 +			SOME (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
   1.142  		    end
   1.143 -		  | None => process thms
   1.144 +		  | NONE => process thms
   1.145  	    end
   1.146  	    handle e as THM _ => process thms
   1.147      in
   1.148  	fn thms =>
   1.149  	   case process thms of
   1.150 -	       res as Some (name,th) => if (prop_of th) aconv t
   1.151 +	       res as SOME (name,th) => if (prop_of th) aconv t
   1.152  					then res
   1.153  					else error "Internal error in set_prop"
   1.154 -	     | None => None
   1.155 +	     | NONE => NONE
   1.156      end
   1.157      handle e => (writeln "set_prop internal error"; print_exn e)
   1.158  
   1.159 @@ -624,8 +624,8 @@
   1.160  	val set = set_prop thy t
   1.161  	fun process_tac thms st =
   1.162  	    case set thms of
   1.163 -		Some (_,th) => Seq.of_list (compose (th,i,st))
   1.164 -	      | None => Seq.empty
   1.165 +		SOME (_,th) => Seq.of_list (compose (th,i,st))
   1.166 +	      | NONE => Seq.empty
   1.167      in
   1.168  	(process_tac thms APPEND (if search
   1.169  				  then process_tac (find_potential thy t)