Forgot a couple of checks for the quick_and_dirty flag the other day.

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