src/HOL/Import/import_syntax.ML
changeset 17370 754b7fcff03e
parent 17057 0934ac31985f
child 17644 bd59bfd4bf37
     1.1 --- a/src/HOL/Import/import_syntax.ML	Tue Sep 13 22:19:54 2005 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Tue Sep 13 22:21:06 2005 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4      end
     1.5  
     1.6  fun create_int_thms thyname thy =
     1.7 -    if !SkipProof.quick_and_dirty
     1.8 +    if ! quick_and_dirty
     1.9      then thy
    1.10      else
    1.11  	case ImportData.get thy of
    1.12 @@ -164,7 +164,7 @@
    1.13  	  | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?"
    1.14  
    1.15  fun clear_int_thms thy =
    1.16 -    if !SkipProof.quick_and_dirty
    1.17 +    if ! quick_and_dirty
    1.18      then thy
    1.19      else
    1.20  	case ImportData.get thy of