src/HOL/Import/import_syntax.ML
changeset 15531 08c8dad8e399
parent 14627 5d137da82f03
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Import/import_syntax.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -113,8 +113,8 @@
     1.4  				     let
     1.5  					 val thyname = get_import_thy thy
     1.6  				     in
     1.7 -					 foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol false isa thy
     1.8 -						 | (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
     1.9 +					 foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
    1.10 +						 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
    1.11  				     end)
    1.12  
    1.13  val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
    1.14 @@ -123,8 +123,8 @@
    1.15  				      let
    1.16  					  val thyname = get_import_thy thy
    1.17  				      in
    1.18 -					  foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol true isa thy
    1.19 -						  | (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
    1.20 +					  foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
    1.21 +						  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
    1.22  				      end)
    1.23  
    1.24  fun import_thy s =
    1.25 @@ -160,16 +160,16 @@
    1.26      then thy
    1.27      else
    1.28  	case ImportData.get thy of
    1.29 -	    None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy
    1.30 -	  | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?"
    1.31 +	    NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy
    1.32 +	  | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
    1.33  
    1.34  fun clear_int_thms thy =
    1.35      if !SkipProof.quick_and_dirty
    1.36      then thy
    1.37      else
    1.38  	case ImportData.get thy of
    1.39 -	    None => error "Import data already cleared - forgotten a setup_theory?"
    1.40 -	  | Some _ => ImportData.put None thy
    1.41 +	    NONE => error "Import data already cleared - forgotten a setup_theory?"
    1.42 +	  | SOME _ => ImportData.put NONE thy
    1.43  
    1.44  val setup_theory = P.name
    1.45  		       >>