Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
global quick_and_dirty;
authorwenzelm
Tue, 13 Sep 2005 22:21:06 +0200
changeset 17370 754b7fcff03e
parent 17369 dec2ddbb3edf
child 17371 923ef4a8c672
global quick_and_dirty;
src/HOL/Import/import_package.ML file | annotate | diff | comparison | revisions
src/HOL/Import/import_syntax.ML file | annotate | diff | comparison | revisions 
--- 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 =>
--- 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
isabelle