src/HOL/Tools/record.ML
changeset 32970 fbd2bb2489a8
parent 32957 675c0c7e6a37
child 32972 45ba8b02e1e4
     1.1 --- a/src/HOL/Tools/record.ML	Sat Oct 17 16:40:41 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 16:58:03 2009 +0200
     1.3 @@ -1040,7 +1040,7 @@
     1.4    if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
     1.5      Goal.prove (ProofContext.init thy) [] []
     1.6        (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
     1.7 -      (K (SkipProof.cheat_tac @{theory HOL}))
     1.8 +      (K (Skip_Proof.cheat_tac @{theory HOL}))
     1.9        (*Drule.standard can take quite a while for large records, thats why
    1.10          we varify the proposition manually here.*)
    1.11    else