Forgot a couple of checks for the quick_and_dirty flag the other day.
authorskalberg
Mon Apr 19 10:57:26 2004 +0200 (2004-04-19)
changeset 146275d137da82f03
parent 14626 dfb8d2977263
child 14628 8086e5beef0e
Forgot a couple of checks for the quick_and_dirty flag the other day.
src/HOL/Import/import_syntax.ML
     1.1 --- a/src/HOL/Import/import_syntax.ML	Mon Apr 19 09:31:00 2004 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Mon Apr 19 10:57:26 2004 +0200
     1.3 @@ -156,14 +156,20 @@
     1.4      end
     1.5  
     1.6  fun create_int_thms thyname thy =
     1.7 -    case ImportData.get thy of
     1.8 -	None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy
     1.9 -      | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?"
    1.10 +    if !SkipProof.quick_and_dirty
    1.11 +    then thy
    1.12 +    else
    1.13 +	case ImportData.get thy of
    1.14 +	    None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy
    1.15 +	  | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?"
    1.16  
    1.17  fun clear_int_thms thy =
    1.18 -    case ImportData.get thy of
    1.19 -	None => error "Import data already cleared - forgotten a setup_theory?"
    1.20 -      | Some _ => ImportData.put None thy
    1.21 +    if !SkipProof.quick_and_dirty
    1.22 +    then thy
    1.23 +    else
    1.24 +	case ImportData.get thy of
    1.25 +	    None => error "Import data already cleared - forgotten a setup_theory?"
    1.26 +	  | Some _ => ImportData.put None thy
    1.27  
    1.28  val setup_theory = P.name
    1.29  		       >>