1.1 --- a/src/HOL/Import/import.ML	Sat Oct 17 16:40:41 2009 +0200
     1.2 +++ b/src/HOL/Import/import.ML	Sat Oct 17 16:58:03 2009 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  fun import_tac ctxt (thyname, thmname) =
     1.6      if ! quick_and_dirty
     1.7 -    then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
     1.8 +    then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
     1.9      else
    1.10       fn th =>
    1.11          let