src/HOL/Import/replay.ML
changeset 15531 08c8dad8e399
parent 14620 1be590fd2422
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Import/replay.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -57,8 +57,8 @@
     1.4  	  | rp (PHyp tm) thy = P.ASSUME tm thy
     1.5  	  | rp (PDef(seg,name,rhs)) thy =
     1.6  	    (case P.get_def seg name rhs thy of
     1.7 -		 (thy',Some res) => (thy',res)
     1.8 -	       | (thy',None) => 
     1.9 +		 (thy',SOME res) => (thy',res)
    1.10 +	       | (thy',NONE) => 
    1.11  		 if seg = thyname
    1.12  		 then P.new_definition seg name rhs thy'
    1.13  		 else raise ERR "replay_proof" "Too late for term definition")
    1.14 @@ -208,25 +208,25 @@
    1.15  	    in
    1.16  		case pc of
    1.17  		    PDisk => (case disk_info_of p of
    1.18 -				  Some(thyname',thmname) =>
    1.19 +				  SOME(thyname',thmname) =>
    1.20  				  (case Int.fromString thmname of
    1.21  				       SOME i =>
    1.22  				       if thyname' = thyname
    1.23  				       then
    1.24  					   (case Array.sub(int_thms,i-1) of
    1.25 -						None =>
    1.26 +						NONE =>
    1.27  						let
    1.28  						    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
    1.29 -						    val _ = Array.update(int_thms,i-1,Some th)
    1.30 +						    val _ = Array.update(int_thms,i-1,SOME th)
    1.31  						in
    1.32  						    (thy',th)
    1.33  						end
    1.34 -					      | Some th => (thy,th))
    1.35 +					      | SOME th => (thy,th))
    1.36  				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
    1.37  				     | NONE => 
    1.38  				       (case P.get_thm thyname' thmname thy of
    1.39 -					    (thy',Some res) => (thy',res)
    1.40 -					  | (thy',None) => 
    1.41 +					    (thy',SOME res) => (thy',res)
    1.42 +					  | (thy',NONE) => 
    1.43  					    if thyname' = thyname
    1.44  					    then
    1.45  						let
    1.46 @@ -242,11 +242,11 @@
    1.47  						      | _ => P.store_thm thyname' thmname th thy'
    1.48  						end
    1.49  					    else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
    1.50 -				| None => raise ERR "rp'.PDisk" "Not enough information")
    1.51 +				| NONE => raise ERR "rp'.PDisk" "Not enough information")
    1.52  		  | PAxm(name,c) =>
    1.53  		    (case P.get_axiom thyname name thy of
    1.54 -			    (thy',Some res) => (thy',res)
    1.55 -			  | (thy',None) => P.new_axiom name c thy')
    1.56 +			    (thy',SOME res) => (thy',res)
    1.57 +			  | (thy',NONE) => P.new_axiom name c thy')
    1.58  		  | PTmSpec(seg,names,prf') =>
    1.59  		    let
    1.60  			val (thy',th) = rp' prf' thy
    1.61 @@ -275,8 +275,8 @@
    1.62      let
    1.63  	val fname =
    1.64  	    case P.get_proof_dir thyname thy of
    1.65 -		Some p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
    1.66 -	      | None => error "Cannot find proof files"
    1.67 +		SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
    1.68 +	      | NONE => error "Cannot find proof files"
    1.69  	val is = TextIO.openIn fname
    1.70  	val (num_int_thms,facts) =
    1.71  	    let
    1.72 @@ -290,7 +290,7 @@
    1.73  		get_facts []
    1.74  	    end
    1.75  	val _ = TextIO.closeIn is
    1.76 -	val int_thms = Array.array(num_int_thms,None:thm option)
    1.77 +	val int_thms = Array.array(num_int_thms,NONE:thm option)
    1.78      in
    1.79  	(int_thms,facts)
    1.80      end