# 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
 		       >>