# HG changeset patch
# User wenzelm
# Date 1126642866 -7200
# Node ID 754b7fcff03e9a3aca3a37123629922c80f167cc
# Parent  dec2ddbb3edf6bbc957b6ff95c4ee5565bc6b811
global quick_and_dirty;

diff -r dec2ddbb3edf -r 754b7fcff03e src/HOL/Import/import_package.ML
--- a/src/HOL/Import/import_package.ML	Tue Sep 13 22:19:54 2005 +0200
+++ b/src/HOL/Import/import_package.ML	Tue Sep 13 22:21:06 2005 +0200
@@ -33,7 +33,7 @@
 val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
 
 fun import_tac (thyname,thmname) =
-    if !SkipProof.quick_and_dirty
+    if ! quick_and_dirty
     then SkipProof.cheat_tac
     else
      fn thy =>
diff -r dec2ddbb3edf -r 754b7fcff03e src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Tue Sep 13 22:19:54 2005 +0200
+++ b/src/HOL/Import/import_syntax.ML	Tue Sep 13 22:21:06 2005 +0200
@@ -156,7 +156,7 @@
     end
 
 fun create_int_thms thyname thy =
-    if !SkipProof.quick_and_dirty
+    if ! quick_and_dirty
     then thy
     else
 	case ImportData.get thy of
@@ -164,7 +164,7 @@
 	  | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
 
 fun clear_int_thms thy =
-    if !SkipProof.quick_and_dirty
+    if ! quick_and_dirty
     then thy
     else
 	case ImportData.get thy of