# HG changeset patch # User skalberg # Date 1082365046 -7200 # Node ID 5d137da82f03e29012d6ef110aa91ead922a869a # Parent dfb8d2977263726477cc0fc69e47ac707cef2faf Forgot a couple of checks for the quick_and_dirty flag the other day. diff -r dfb8d2977263 -r 5d137da82f03 src/HOL/Import/import_syntax.ML --- a/src/HOL/Import/import_syntax.ML Mon Apr 19 09:31:00 2004 +0200 +++ b/src/HOL/Import/import_syntax.ML Mon Apr 19 10:57:26 2004 +0200 @@ -156,14 +156,20 @@ end fun create_int_thms thyname thy = - case ImportData.get thy of - None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy - | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?" + if !SkipProof.quick_and_dirty + then thy + else + case ImportData.get thy of + None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy + | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?" fun clear_int_thms thy = - case ImportData.get thy of - None => error "Import data already cleared - forgotten a setup_theory?" - | Some _ => ImportData.put None thy + if !SkipProof.quick_and_dirty + then thy + else + case ImportData.get thy of + None => error "Import data already cleared - forgotten a setup_theory?" + | Some _ => ImportData.put None thy val setup_theory = P.name >>